Proof.

For every sets

X

2

P

(

Src

f

)

,

Y

2

P

(

Dst

f

)

X

[(

FCD

)(

RLD

)

in

f

]

Y

,

"

Src

f

X

RLD

"

Dst

f

Y

/ (

RLD

)

in

f

,

"

RLD

(

Src

f

;

Dst

f

)

(

X

Y

)

/

a

RLD

b

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; a

FCD

b

v

f

,

(*)

9

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

: (

a

FCD

b

v

f

^

a

v "

Src

f

X

^

b

v "

Dst

f

Y

)

,

X

[

f

]

Y :

* proposition

4.215

.

Thus

(

FCD

)(

RLD

)

in

f

=

f

.

Remark 8.21.

The above theorem allows to represent funcoids as reloids.

Obvious 8.22.

(

RLD

)

in

(

FCD

B

) =

RLD

B

for every lters

A

,

B

.

Conjecture 8.23.

(

RLD

)

out

id

A

FCD

=

id

A

RLD

for every lter

A

.

Exercise 8.1.

Prove that generally

(

RLD

)

in

id

A

FCD

=

/

id

A

RLD

.

Conjecture 8.24.

dom

(

RLD

)

in

f

=

dom

f

and im

(

RLD

)

in

f

=

im

f

for every funcoid

f

.

[TODO:

easy using products of ultralters?]

Proposition 8.25.

dom

(

f

j

A

) =

A u

dom

f

for every reloid

f

and lter

A 2

F

(

Src

f

)

.

Proof.

dom

(

f

j

A

) =

dom

(

FCD

)(

f

j

A

) =

dom

((

FCD

)

f

)

j

A

=

A u

dom

(

FCD

)

f

=

A u

dom

f

.

Theorem 8.26.

For every composable reloids

f

,

g

:

1. If im

f

w

dom

g

then im

(

g

f

) =

im

g

.

2. If im

f

v

dom

g

then dom

(

g

f

) =

dom

g

.

Proof.

1. im

(

g

f

) =

im

(

FCD

)(

g

f

) =

im

((

FCD

)

g

(

FCD

)

f

) =

im

(

FCD

)

g

=

im

g

.

2. Similar.

Conjecture 8.27.

(

RLD

)

in

(

g

f

) = (

RLD

)

in

g

(

RLD

)

in

f

for every composable funcoids

f

and

g

.

[TODO: Solved.]

Theorem 8.28.

a

RLD

b

v

(

RLD

)

in

f

,

a

FCD

b

v

f

for every funcoid

f

and

a

2

atoms

F

(

Src

f

)

,

b

2

atoms

F

(

Dst

f

)

.

[TODO: Move to funcoidal reloids section?]

Proof.

a

FCD

b

v

f

)

a

RLD

b

v

(

RLD

)

in

f

is obvious.

a

RLD

b

v

(

RLD

)

in

f

)

a

RLD

b

/ (

RLD

)

in

f

)

a

[(

FCD

)(

RLD

)

in

f

]

b

)

a

[

f

]

b

)

a

FCD

b

v

f

.

Conjecture 8.29.

If

RLD

B v

(

RLD

)

in

f

then

FCD

B v

f

for every funcoid

f

and

A 2

F

(

Src

f

)

,

B 2

F

(

Dst

f

)

.

Theorem 8.30.

GR

(

FCD

)

g

GR

g

for every reloid

g

.

Proof.

Let

K

2

GR

g

. Then for every sets

X

2

P

Src

g

,

Y

2

P

Dst

g

X

[

K

]

Y

,

X

[

"

FCD

K

]

Y

,

X

[(

FCD

)

"

RLD

K

]

Y

(

X

[(

FCD

)

g

]

Y

.

Thus

"

FCD

K

w

(

FCD

)

g

that is

K

2

GR

(

FCD

)

g

.

Theorem 8.31.

g

(

RLD

B

)

f

=

h

(

FCD

)

f

¡

1

iA

RLD

h

(

FCD

)

g

iB

for every reloids

f

,

g

and

lters

A 2

F

(

Dst

f

)

,

B 2

F

(

Src

g

)

.

[TODO: Similar proposition for funcoids?]

8.2 Reloids induced by a funcoid

135