 Suppose

F

2

up

(

RLD

)

¡

=

up

d

RLD

up

¡(

Src

f

;

Dst

f

)

f

. Then by properties of generalized lter

bases, there is

F

0

2

up

¡(

Src

f

;

Dst

f

)

f

such that

F

F

0

. Because

F

0

S

i

2

Z

([

i

;

i

+ 1[

[

i

;

i

+ 1[)

and

F

0

(=)

j

R

, there is a point

q

2

[

i

;

i

+ 1[

[

i

;

i

+ 1[

for each

i

2

Z

; thus,

F

0

2

/ ¡(

Src

f

;

Dst

f

)

.

Thus

F

2

/

up

(

RLD

)

¡

f

.

Theorem 39.

For every reloid

f

and

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

:

1.

X

[(

FCD

)

f

]

Y , 8

F

2

up

¡(

Src

f

;

Dst

f

)

f

:

X

[

F

]

Y

;

2.

h

(

FCD

)

f

iX

=

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

iX

.

Proof.

1.

8

F

2

up

¡(

Src

f

;

Dst

f

)

f

:

X

[

F

]

Y ,

(by properties of generalized lter bases, taking into

account that funcoids are isomorphic to lters)

,X

d

FCD

up

¡(

Src

f

;

Dst

f

)

f

Y , X

[(

FCD

)

f

]

Y

.

2.

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

i

a

=

d

FCD

up

¡(

Src

f

;

Dst

f

)

f

a

=

h

(

FCD

)

f

i

a

for every ultralter

a

.

It remains to prove that the function

'

=

X 2

F

(

Src

f

):

l

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

iX

is a component of a funcoid (from what follows that

'

=

h

(

FCD

)

f

i

). To prove this, it's enough to

show that it preserves nite joins and ltered meets.

[TODO: Denition of ltered meets.]

'

0 = 0

is obvious.

'

(

I t J

) =

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

(

h

F

iI t h

F

iJ

) =

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

iI t

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

iJ

=

'

I t

'

J

. If

S

is a generalized lter base of Src

f

, then

'

d

F

S

=

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

i

d

F

S

=

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

d

F

hh

F

ii

S

=

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

d

X 2

S

F

h

F

iX

=

d

X 2

S

F

d

F

2

up

¡(

Src

f

;

Dst

f

)

f

F

h

F

iX

=

d

X 2

S

F

'

X

=

d

F

h

'

i

S

.

So

'

is a component of a funcoid.

Denition 40.

f

=

d

RLD

up

¡(

Src

f

;

Dst

f

)

f

for reloid

f

.

Conjecture 41.

For every reloid

f

:

1.

f

= (

RLD

)

in

(

FCD

)

f

;

2.

f

= (

RLD

)

¡

(

FCD

)

f

.

Obvious 42.

f

w

f

for every reloid

f

.

Example 43.

(

RLD

)

¡

f

=

/

(

RLD

)

out

f

for some funcoid

f

.

Proof.

Take

f

=

id

(

N

)

FCD

. Then, as it was shown above,

(

RLD

)

out

f

= 0

and thus

(

RLD

)

out

f

= 0

.

But

(

RLD

)

¡

f

w

(

RLD

)

in

f

=

/ 0

. So

(

RLD

)

¡

f

=

/

(

RLD

)

out

f

.

Conjecture 44.

(

RLD

)

¡

f

=

(

RLD

)

in

f

for every funcoid

f

.

Proposition 45.

[TODO: Move it above in the book.]

f

v A

FCD

B ,

dom

f

v A ^

im

f

v B

for

every funcoid

f

and lters

A 2

F

(

Src

f

)

,

B 2

F

(

Dst

f

)

.

Proof.

f

v A

FCD

B )

dom

f

v A

because dom

(

FCD

B

)

v A

.

Let now dom

f

v A ^

im

f

v B

. Then

h

f

iX

=

/ 0

) X

/

A

that is

f

v A

FCD

1

. Similarly

f

v

1

FCD

B

. Thus

f

v A

FCD

B

.

Theorem 46.

dom

(

RLD

)

in

f

=

dom

f

and im

(

RLD

)

in

f

=

im

f

for every funcoid

f

.

[TODO: Move

it above in the book, remove the conjecture which this statement proves.]

Proof.

We have for every lter

X 2

F

(

Src

f

)

:

X w

dom

(

RLD

)

in

f

, X

RLD

1

w

(

RLD

)

in

f

, 8

a

2

F

(

Src

f

)

; b

2

F

(

Dst

f

): (

a

FCD

b

v

f

)

a

RLD

b

v X

RLD

1)

, 8

a

2

F

(

Src

f

)

; b

2

F

(

Dst

f

): (

a

FCD

b

v

f

)

a

v X

)

;

8

Section 6