 but this is the statement of the lemma.

9.5 Embedding reloids into funcoids

Denition 9.8.

Let

f

be a reloid. The funcoid

f

2

FCD

(

P

(

Src

f

Src

f

);

P

(

Dst

f

Dst

f

))

is dened by the formulas:

h

f

i

x

=

f

x

and

h

f

¡

1

i

y

=

f

¡

1

y

where

x

are endoreloids on Src

f

and

y

are endoreloids on Dst

f

.

Proposition 9.9.

It is really a funcoid (if we equate reloids

x

and

y

with corresponding lters on

Cartesian products of sets).

Proof.

y

/

h

f

i

x

,

y

/

f

x

,

f

¡

1

y

/

x

, h

f

¡

1

i

y

/

x

.

Corollary 9.10.

(

f

)

¡

1

=

f

¡

1

.

Denition 9.11.

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 9.12.

is an injection.

Proof.

Consider

x

=

id

Src

f

.

Proposition 9.13.

(

g

f

) = (

g

)

(

f

)

.

Proof.

h

(

g

f

)

i

x

=

g

f

x

=

h

g

ih

f

i

x

= (

h

g

i  h

f

i

)

x

. Thus

h

(

g

f

)

i

=

h

g

i  h

f

i

=

h

(

g

)

(

f

)

i

and so

(

g

f

) = (

g

)

(

f

)

.

Theorem 9.14.

F

F

=

F

h

i

F

for a set

F

of reloids.

Proof.

It's enough to prove

h

F

F

i

X

=

h

F

h

i

F

i

X

for a set

X

.

Really,

h

F

F

i

X

=

h

F

F

i"

X

=

F

F

"

X

=

F

f

f

"

X

j

f

2

F

g

=

F

fh

f

i"

X

j

f

2

F

g

=

h

F

f

f

j

f

2

F

gi"

X

=

h

F

h

i

F

i

X

.

Conjecture 9.15.

d

F

=

d

h

i

F

for a set

F

of reloids.

Proposition 9.16.

id

RLD

(

A

)

=

id

FCD

(

P

(

A

A

))

.

Proof.

id

RLD

(

A

)

x

=

id

RLD

(

A

)

x

=

x

.

We can try to develop further theory by applying embedding of reloids into funcoids for

researching of properties of reloids.

Theorem 9.17.

Reloid

f

is monovalued i funcoid

f

is monovalued.

Proof.

f

is monovalued

,

(

f

)

(

f

)

¡

1

v

1

Dst

f

,

(

f

f

¡

1

)

v

1

Dst

f

,

(

f

f

¡

1

)

v

id

FCD

(

P

(

Dst

f

Dst

f

))

,

(

f

f

¡

1

)

v

id

RLD

(

Dst

f

)

,

f

f

¡

1

v

id

RLD

(

Dst

f

)

,

f

is monovalued.

9.5 Embedding reloids into funcoids

141