9.1. FUNCOID INDUCED BY A RELOID

198

Proof.

X ×

RLD

Y 6

f

F

up

f, P

up(

X ×

RLD

Y

) :

P

6

F

F

up

f, X

up

X

, Y

up

Y

:

X

×

Y

6

F

F

up

f, X

up

X

, Y

up

Y

:

X

FCD

F

Y

F

up

f

:

X

FCD

F

Y ⇔

X

[(

FCD

)

f

]

Y

.

Theorem

1063

.

(

FCD

)

f

=

d

FCD

up

f

for every reloid

f

.

Proof.

Let

a

be an ultrafilter on Src

f

.

h

(

FCD

)

f

i

a

=

d

h

FCD

F

i

a

F

up

f

by the definition of (

FCD

).

D

d

FCD

up

f

E

a

=

d

h

FCD

F

i

a

F

up

f

by theorem

875

.

So

h

(

FCD

)

f

i

a

=

D

d

FCD

up

f

E

a

for every ultrafilter

a

.

Lemma

1064

.

For every two filter bases

S

and

T

of morphisms

Rel

(

U, V

) and

every typed set

A

T

U

RLD

l

S

=

RLD

l

T

F

l

F

S

h

F

i

A

=

F

l

G

T

h

G

i

A.

Proof.

Let

d

RLD

S

=

d

RLD

T

.

First let prove that

n

h

F

i

A

F

S

o

is a filter base. Let

X, Y

n

h

F

i

A

F

S

o

. Then

X

=

h

F

X

i

A

and

Y

=

h

F

Y

i

A

for some

F

X

, F

Y

S

. Because

S

is a filter base,

we have

S

3

F

Z

v

F

X

u

F

Y

. So

h

F

Z

i

A

v

X

u

Y

and

h

F

Z

i

A

n

h

F

i

A

F

S

o

. So

n

h

F

i

A

F

S

o

is a filter base.

Suppose

X

up

d

F

F

S

h

F

i

A

. Then there exists

X

0

n

h

F

i

A

F

S

o

where

X

w

X

0

because

n

h

F

i

A

F

S

o

is a filter base. That is

X

0

=

h

F

i

A

for some

F

S

. There

exists

G

T

such that

G

v

F

because

T

is a filter base. Let

Y

0

=

h

G

i

A

. We

have

Y

0

v

X

0

v

X

;

Y

0

n

h

G

i

A

G

T

o

;

Y

0

up

d

F

G

T

h

G

i

A

;

X

up

d

F

G

T

h

G

i

A.

The reverse is symmetric.

Lemma

1065

.

n

G

F

F

up

f,G

up

g

o

is a filter base for every reloids

f

and

g

.

Proof.

Let denote

D

=

n

G

F

F

up

f,G

up

g

o

. Let

A

D

B

D

. Then

A

=

G

A

F

A

B

=

G

B

F

B

for some

F

A

, F

B

up

f

,

G

A

, G

B

up

g

. So

A

u

B

w

(

G

A

u

G

B

)

(

F

A

u

F

B

)

D

because

F

A

u

F

B

up

f

and

G

A

u

G

B

up

g

.

Theorem

1066

.

(

FCD

)(

g

f

) = ((

FCD

)

g

)

((

FCD

)

f

) for every composable

reloids

f

and

g

.

Proof.

h

(

FCD

)(

g

f

)

i

X

=

F

l

H

up(

g

f

)

h

H

i

X

=

F

l

H

up

d

RLD

{

G

F

F

up

f,G

up

g

}

h

H

i

X.