9.1. FUNCOID INDUCED BY A RELOID

199

Obviously

RLD

l

G

F

F

up

f, G

up

g

=

RLD

l

up

RLD

l

G

F

F

up

f, G

up

g

;

from this by lemma

1064

(taking into account that

G

F

F

up

f, G

up

g

and

up

RLD

l

G

F

F

up

f, G

up

g

are filter bases)

RLD

l

H

up

d

RLD

{

G

F

F

up

f,G

up

g

}

h

H

i

X

=

F

l

h

G

F

i

X

F

up

f, G

up

g

.

On the other side

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

=

h

(

FCD

)

g

ih

(

FCD

)

f

i

X

=

h

(

FCD

)

g

i

F

l

F

up

f

h

F

i

X

=

l

G

up

g

FCD

G

RLD

l

F

up

f

h

F

i

X.

Let’s prove that

n

h

F

i

X

F

up

f

o

is a filter base. If

A, B

n

h

F

i

X

F

up

f

o

then

A

=

h

F

1

i

X

,

B

=

h

F

2

i

X

where

F

1

, F

2

up

f

.

A

u

B

w h

F

1

u

F

2

i

X

n

h

F

i

X

F

up

f

o

. So

n

h

F

i

X

F

up

f

o

is really a filter base.

By theorem

836

we have

FCD

G

F

l

F

up

f

h

F

i

X

=

F

l

F

up

f

h

G

i

h

F

i

X.

So continuing the above equalities,

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

=

F

l

G

up

g

F

l

F

up

f

h

G

i

h

F

i

X

=

F

l

h

G

i

h

F

i

X

F

up

f, G

up

g

=

F

l

h

G

F

i

X

F

up

f, G

up

g

.

Combining these equalities we get

h

(

FCD

)(

g

f

)

i

X

=

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

for every typed set

X

T

(Src

f

).

Proposition

1067

.

(

FCD

) id

RLD

A

= id

FCD

A

for every filter

A

.