9.2. RELOIDS INDUCED BY A FUNCOID

201

Proof.

im(

FCD

)

f

=

h

(

FCD

)

f

i>

=

F

l

F

up

f

h

F

i

>

=

F

l

F

up

f

im

F

=

F

l

h

im

i

up

f

= im

f.

dom(

FCD

)

f

= dom

f

is similar.

Proposition

1073

.

(

FCD

)(

f

u

(

A ×

RLD

B

)) = (

FCD

)

f

u

(

A ×

FCD

B

) for every

reloid

f

and

A ∈

F

(Src

f

) and

B ∈

F

(Dst

f

).

Proof.

(

FCD

)(

f

u

(

A ×

RLD

B

)) =

(

FCD

)(id

RLD

B

f

id

RLD

A

) =

(

FCD

) id

RLD

B

(

FCD

)

f

(

FCD

) id

RLD

A

=

id

FCD

B

(

FCD

)

f

id

FCD

A

=

(

FCD

)

f

u

(

A ×

FCD

B

)

.

Corollary

1074

.

(

FCD

)(

f

|

A

) = ((

FCD

)

f

)

|

A

for every reloid

f

and a filter

A ∈

F

(Src

f

).

Proposition

1075

.

h

(

FCD

)

f

iX

= im(

f

|

X

) for every reloid

f

and a filter

X ∈

F

(Src

f

).

Proof.

im(

f

|

X

) = im(

FCD

)(

f

|

X

) = im(((

FCD

)

f

)

|

X

) =

h

(

FCD

)

f

iX

.

Proposition

1076

.

(

FCD

)

f

=

d

n

x

×

FCD

y

x

atoms

F

(Src

f

)

,y

atoms

F

(Dst

f

)

,x

×

RLD

y

6

f

o

for

every reloid

f

.

Proof.

(

FCD

)

f

=

d

n

x

×

FCD

y

x

atoms

F

(Src

f

)

,y

atoms

F

(Dst

f

)

,x

×

FCD

y

6

(

FCD

)

f

o

, but

x

×

FCD

y

6

(

FCD

)

f

x

[(

FCD

)

f

]

y

x

×

RLD

y

6

f

, thus follows the theorem.

9.2. Reloids induced by a funcoid

Every funcoid

f

FCD

(

A, B

) induces a reloid from

A

to

B

in two ways,

intersection of

outward

relations and union of

inward

reloidal products of filters:

(

RLD

)

out

f

=

RLD

l

up

f

;

(

RLD

)

in

f

=

l

A ×

RLD

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

.

Theorem

1077

.

(

RLD

)

in

f

=

d

n

a

×

RLD

b

a

atoms

F

(

A

)

,b

atoms

F

(

B

)

,a

×

FCD

b

v

f

o

.

Proof.

It follows from theorem

1011

.

Proposition

1078

.

up

RLD

f

= up

FCD

f

for every

Rel

-morphism

f

.

Proof.

X

up

RLD

f

X

w

f

X

up

FCD

f

.

Proposition

1079

.

(

RLD

)

out

FCD

f

=

RLD

f

for every

Rel

-morphism

f

.

Proof.

(

RLD

)

out

FCD

f

=

d

RLD

up

f

=

RLD

min up

f

=

RLD

f

taking into

account the previous proposition.