10.5. EMBEDDING RELOIDS INTO FUNCOIDS

217

K

n

0

f

)

∩···∩

n

f

)

n

N

o

. So

K

0

0

f

)

∩ · · · ∩

0

n

f

)

n

N

,

Γ

0

i

up

d

T

=

0

0

∩ · · · ∩

Γ

0

n

)

f

n

N

,

Γ

0

i

up

d

T

=

up

RLD

(Src

f

×

V,

f

)

l

G

f

G

up

d

T

.

10.4. Proof of the main result

Let’s prove a special case of conjecture

1058

:

Theorem

1163

.

(

d

T

)

F

=

d

G

F

G

T

for every principal reloid

F

=

RLD

f

(for a

Rel

-morphism

f

) and a set

T

of reloids from Dst

F

to some set

V

. (In

other words principal reloids are co-metacomplete and thus also metacomplete by

duality.)

Proof.

l

T

F

=

RLD

(Src

f,V

)

l

h

dom

i

l

T

F

=

dom

RLD

(Src

f

×

V,

f

)

l

l

T

F

=

dom

RLD

(Src

f

×

V,

f

)

l

G

up

d

T

(

G

f

);

l

G

T

(

G

F

) =

l

G

T

RLD

(Src

f,V

)

l

h

dom

i

(

G

F

) =

l

G

T

dom

RLD

(Src

f

×

V,

f

)

l

(

G

F

) =

dom

l

G

T

RLD

(Src

f

×

V,

f

)

l

(

G

F

)

.

It’s enough to prove

RLD

(Src

f

×

V,

f

)

l

G

up

d

T

(

G

f

) =

l

G

T

RLD

(Src

f

×

V,

f

)

l

(

G

F

)

but this is the statement of the lemma.

10.5. Embedding reloids into funcoids

Definition

1164

.

Let

f

be a reloid. The funcoid

ρf

=

FCD

(

P

(Src

f

×

Src

f

)

,

P

(Dst

f

×

Dst

f

))