8.2. RELOIDS INDUCED BY A FUNCOID

152

Proof.

For every sets

X

P

(Src

f

),

Y

P

(Dst

f

)

X

[(

FCD

)(

RLD

)

in

f

]

Y

Src

f

X

×

RLD

Dst

f

Y

6

(

RLD

)

in

f

RLD

(Src

f

;Dst

f

)

(

X

×

Y

)

6

G

a

×

RLD

b

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, a

×

FCD

b

v

f

(*)

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

: (

a

×

FCD

b

v

f

a

v↑

Src

f

X

b

v↑

Dst

f

Y

)

X

[

f

]

Y.

* proposition

482

.

Thus (

FCD

)(

RLD

)

in

f

=

f

.

Remark

819

.

The above theorem allows to represent funcoids as reloids.

FiXme

:

Refer to “funcoidal reloids” defined below.

Obvious

820

.

(

RLD

)

in

(

A ×

FCD

B

) =

A ×

RLD

B

for every filters

A

,

B

.

Conjecture

821

.

(

RLD

)

out

id

FCD

A

= id

RLD

A

for every filter

A

.

Exercise

822

.

Prove that generally (

RLD

)

in

id

FCD

A

6

= id

RLD

A

.

Conjecture

823

.

dom(

RLD

)

in

f

= dom

f

and im(

RLD

)

in

f

= im

f

for every

funcoid

f

.

FiXme

: easy using products of ultrafilters?

Proposition

824

.

dom(

f

|

A

) =

A u

dom

f

for every reloid

f

and filter

A ∈

F

(Src

f

).

Proof.

dom(

f

|

A

) = dom(

FCD

)(

f

|

A

) = dom((

FCD

)

f

)

|

A

=

A u

dom(

FCD

)

f

=

A u

dom

f

.

Theorem

825

.

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

826

.

(

RLD

)

in

(

g

f

) = (

RLD

)

in

g

(

RLD

)

in

f

for every composable

funcoids

f

and

g

.

FiXme

: Solved.

Theorem

827

.

a

×

RLD

b

v

(

RLD

)

in

f

a

×

FCD

b

v

f

for every funcoid

f

and

a

atoms

F

(Src

f

)

,

b

atoms

F

(Dst

f

)

.

FiXme

: 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

6

(

RLD

)

in

f

a

[(

FCD

)(

RLD

)

in

f

]

b

a

[

f

]

b

a

×

FCD

b

v

f.

Conjecture

828

.

If

RLD

B v

(

RLD

)

in

f

then

FCD

B v

f

for every funcoid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Theorem

829

.

GR(

FCD

)

g

GR

g

for every reloid

g

.