 8.4. FUNCOIDAL RELOIDS

156

Definition

845

.

I call (

RLD

)

in

(

FCD

)

f

funcoidization

of a reloid

f

.

Lemma

846

.

(

RLD

)

in

(

FCD

)

f

is funcoidal for every reloid

f

.

Proof.

x

×

RLD

y

6

(

RLD

)

in

(

FCD

)

f

x

×

RLD

y

v

(

RLD

)

in

(

FCD

)

f

.

Theorem

847

.

(

RLD

)

in

is a bijection from

FCD

(

A

;

B

) to the set of funcoidal

reloids from

A

to

B

.

Proof.

Let

f

FCD

(

A

;

B

). Prove that (

RLD

)

in

f

is funcoidal.

Really (

RLD

)

in

f

= (

RLD

)

in

(

FCD

)(

RLD

)

in

f

and thus we can use the lemma

stating that it is funcoidal.

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

=

G

x

×

RLD

y

x

atoms

F

(Src

ν

)

, y

atoms

F

(Dst

ν

)

, x

×

RLD

y

6

f

=

G

p

atoms(

x

×

RLD

y

)

x

atoms

F

(Src

ν

)

, y

atoms

F

(Dst

ν

)

, x

×

RLD

y

6

f

=

G

p

atoms(

x

×

RLD

y

)

x

atoms

F

(Src

ν

)

, y

atoms

F

(Dst

ν

)

, x

×

RLD

y

v

f

=

G

atoms

f

=

f.

Corollary

848

.

Funcoidal reloids are convex.

Proof.

Every (

RLD

)

in

f

is obviously convex.