 9.5. EMBEDDING RELOIDS INTO FUNCOIDS

159

9.4. Proof of the main result

Theorem

855

.

(

F

T

)

F

=

F

G

F

G

T

for every principal reloid

F

=

RLD

(Src

f

;Dst

g

)

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 dual-

ity.)

Proof.

G

T

F

=

l

D

RLD

(Src

f

;

V

)

E

h

dom

i

G

T

F

=

dom

l

D

RLD

(Src

f

×

V

;

f

)

E

G

T

F

=

dom

l

D

RLD

(Src

f

×

V

;

f

)

E

G

f

G

GR

F

T

;

G

G

F

G

T

=

G

(

d

RLD

(Src

f

;

V

)

h

dom

i

(

G

F

)

G

T

)

=

G

(

dom

d

RLD

(Src

f

;

V

)

(

G

F

)

G

T

)

=

dom

G

(

d

RLD

(Src

f

;

V

)

(

G

F

)

G

T

)

.

It’s enough to prove

l

RLD

(Src

f

×

V

;

f

)

(

G

f

)

G

GR

F

T

=

G

(

d

RLD

(Src

f

×

V

;

f

)

(

G

F

)

G

T

)

but this is the statement of the lemma.

9.5. Embedding reloids into funcoids

Definition

856

.

Let

f

be a reloid. The funcoid

ρf

=

FCD

(

P

(Src

f

×

Src

f

);

P

(Dst

f

×

Dst

f

))

is defined by the formulas:

h

ρf

i

x

=

f

x

and

ρf

1

y

=

f

1

y

where

x

are endoreloids on Src

f

and

y

are endoreloids on Dst

f

.

Proposition

857

.

It is really a funcoid (if we equate reloids

x

and

y

with

corresponding filters on Cartesian products of sets).

Proof.

y

6 h

ρf

i

x

y

6

f

x

f

1

y

6

x

ρf

1

y

6

x

.

Corollary

858

.

(

ρf

)

1

=

ρf

1

.

Definition

859

.

It can be continued to arbitrary funcoids

x

having destination

Src

f

by the formula

h

ρ

f

i

x

=

h

ρf

i

id

Src

f

x

=

f

x

.

Proposition

860

.

ρ

is an injection.

Proof.

Consider

x

= id

Src

f

.

Proposition

861

.

ρ

(

g

f

) = (

ρg

)

(

ρf

).