 9.4. FUNCOIDAL RELOIDS

208

It remains to prove (

RLD

)

in

(

FCD

)

f

=

f

for a funcoidal reloid

f

.

((

FCD

)(

RLD

)

in

g

=

g

for every funcoid

g

is already proved above.)

(

RLD

)

in

(

FCD

)

f

=

l

x

×

RLD

y

x

atoms

F

(Src

f

)

, y

atoms

F

(Dst

f

)

, x

×

RLD

y

6

f

=

l

p

atoms(

x

×

RLD

y

)

x

atoms

F

(Src

f

)

, y

atoms

F

(Dst

f

)

, x

×

RLD

y

6

f

=

l

p

atoms(

x

×

RLD

y

)

x

atoms

F

(Src

f

)

, y

atoms

F

(Dst

f

)

, x

×

RLD

y

v

f

=

l

atoms

f

=

f.

Corollary

1117

.

Funcoidal reloids are convex.

Proof.

Every (

RLD

)

in

f

is obviously convex.

Theorem

1118

.

(

RLD

)

in

(

g

f

) = (

RLD

)

in

g

(

RLD

)

in

f

for every composable

funcoids

f

and

g

.

Proof.

(

RLD

)

in

g

(

RLD

)

in

f

= (corollary

1008

=

RLD

l

G

F

F

atoms(

RLD

)

in

f, G

atoms(

RLD

)

in

g

Let

F

be an atom of the poset

RLD

(Src

f,

Dst

f

).

F

atoms(

RLD

)

in

f

dom

F

×

RLD

im

F

6

(

RLD

)

in

f

(because (

RLD

)

in

f

is a funcoidal reloid)

dom

F

×

RLD

im

F

v

(

RLD

)

in

f

but dom

F

×

RLD

im

F

v

(

RLD

)

in

f

F

v

(

RLD

)

in

f

is obvious.

So

F

atoms(

RLD

)

in

f

dom

F

×

RLD

im

F

v

(

RLD

)

in

f

(

FCD

)(dom

F

×

RLD

im

F

)

v

(

FCD

)(

RLD

)

in

f

dom

F

×

FCD

im

F

v

f.

But

dom

F

×

FCD

im

F

v

f

(

RLD

)

in

(dom

F

×

FCD

im

F

)

v

(

RLD

)

in

f

dom

F

×

RLD

im

F

v

(

RLD

)

in

f.

So

F

atoms(

RLD

)

in

f

dom

F

×

FCD

im

F

v

f

.