9.2. RELOIDS INDUCED BY A FUNCOID

203

Proof.

We will prove only dom(

RLD

)

in

f

= dom

f

as the other formula follows

from symmetry. Really:

dom(

RLD

)

in

f

= dom

d

n

a

×

RLD

b

a

atoms

F

(Src

f

)

,b

atoms

F

(Dst

f

)

,a

×

FCD

b

v

f

o

.

By corollary

1030

we have

dom(

RLD

)

in

f

=

l

dom(

a

×

RLD

b

)

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

, a

×

FCD

b

v

f

=

l

dom(

a

×

FCD

b

)

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

, a

×

FCD

b

v

f

.

By corollary

893

we have

dom(

RLD

)

in

f

=

dom

l

a

×

FCD

b

a

atoms

F

(Src

f

)

, b

atoms

F

(Dst

f

)

, a

×

FCD

b

v

f

=

dom

f.

Proposition

1088

.

dom(

f

|

A

) =

A u

dom

f

for every reloid

f

and filter

A ∈

F

(Src

f

).

Proof.

dom(

f

|

A

) = dom(

FCD

)(

f

|

A

) = dom((

FCD

)

f

)

|

A

=

A u

dom(

FCD

)

f

=

A u

dom

f

.

Theorem

1089

.

For every composable reloids

f

,

g

:

1

. If im

f

w

dom

g

then im(

g

f

) = im

g

;

2

. If im

f

v

dom

g

then dom(

g

f

) = dom

f

.

Proof.

1

im(

g

f

) = im(

FCD

)(

g

f

) = im((

FCD

)

g

(

FCD

)

f

) = im(

FCD

)

g

= im

g

.

2

Similar.

Lemma

1090

.

If

a

,

b

,

c

are filters on powersets and

b

6

=

, then

RLD

l

G

F

F

atoms(

a

×

RLD

b

)

, G

atoms(

b

×

RLD

c

)

=

a

×

RLD

c.

Proof.

a

×

RLD

c

= (

b

×

RLD

c

)

(

a

×

RLD

b

) = (corollary

1008

=

RLD

l

G

F

F

atoms(

a

×

RLD

b

)

, G

atoms(

b

×

RLD

c

)

.

Theorem

1091

.

a

×

RLD

b

v

(

RLD

)

in

f

a

×

FCD

b

v

f

for every funcoid

f

and

a

atoms

F

(Src

f

)

,

b

atoms

F

(Dst

f

)

.

Proof.

a

×

FCD

b

v

f

a

×

RLD

b

v

(

RLD

)

in

f

is obvious.