By theorem

6.32

we have

h"

FCD

G

i

l

f"

Dst

g

h

F

i

X

j

F

2

xyGR

f

g

=

l

f"

Dst

g

h

G

ih

F

i

X

j

F

2

xyGR

f

g

:

So continuing the above equalities,

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

=

l

l

f"

Dst

g

h

G

ih

F

i

X

j

F

2

xyGR

f

g j

G

2

xyGR

g

=

l

f"

Dst

g

h

G

ih

F

i

X

j

F

2

xyGR

f ; G

2

xyGR

g

g

=

l

f"

Dst

g

h

G

F

i

X

j

F

2

xyGR

f ; G

2

xyGR

g

g

:

Combining these equalities we get

h

(

FCD

)(

g

f

)

i

X

=

h

((

FCD

)

g

)

((

FCD

)

f

)

i

X

for every set

X

2

P

(

Src

f

)

.

Proposition 8.7.

(

FCD

)

id

A

RLD

=

id

A

FCD

for every lter

A

.

Proof.

Recall that id

A

RLD

=

d

"

Base

(

A

)

id

A

j

A

2 A

. For every

X

;

Y 2

F

(

Base

(

A

))

we have:

X

[(

FCD

)

id

A

RLD

]

Y , X

RLD

/

id

A

RLD

, 8

A

2 A

:

RLD

/

"

RLD

(

Base

(

A

);

Base

(

A

))

id

A

, 8

A

2 A

:

X

"

FCD

(

Base

(

A

);

Base

(

A

))

id

A

Y , 8

A

2 A

:

X u Y

/

"

Base

(

A

)

A

, X u Y

/

A , X

[

id

A

FCD

]

Y

(used

properties of generalized lter bases).

Proposition 8.8.

1.

(

FCD

)

f

is a monovalued funcoid if

f

is a monovalued reloid.

2.

(

FCD

)

f

is an injective funcoid if

f

is an injective reloid.

Proof.

We will prove only the rst as the second is dual. Let

f

be a monovalued reloid. Then

f

f

¡

1

v

id

RLD

(

Dst

f

)

;

(

FCD

)(

f

f

¡

1

)

v

id

FCD

(

Dst

f

)

;

(

FCD

)

f

((

FCD

)

f

)

¡

1

v

id

FCD

(

Dst

f

)

that is

(

FCD

)

f

is a monovalued funcoid.

Proposition 8.9.

(

FCD

)(

RLD

B

) =

FCD

B

for every lters

A

,

B

.

Proof.

X

[(

FCD

)(

RLD

B

)]

Y , 8

F

2

xyGR

(

RLD

B

):

X

[

"

FCD

F

]

Y

(for every

X 2

F

(

Base

(

A

))

,

Y 2

F

(

Base

(

B

))

).

Evidently

8

F

2

xyGR

(

RLD

B

):

X

[

"

FCD

F

]

Y ) 8

A

2 A

; B

2 B

:

X

"

FCD

(

Base

(

A

);

Base

(

B

))

(

A

B

)

Y

.

Let

8

A

2 A

; B

2 B

:

X

"

FCD

(

Base

(

A

);

Base

(

B

))

(

A

B

)

Y

. Then if

F

2

GR

(

RLD

B

)

, there are

A

2 A

,

B

2 B

such that

F

A

B

. So

X

[

"

FCD

F

]

Y

.

We have proved

8

F

2

xyGR

(

RLD

B

):

X

[

"

FCD

F

]

Y , 8

A

2 A

; B

2 B

:

X

"

FCD

(

Base

(

A

);

Base

(

B

))

(

A

B

)

Y

.

Further

8

A

2 A

; B

2 B

:

X

"

FCD

(

Base

(

A

);

Base

(

B

))

(

A

B

)

Y , 8

A

2 A

; B

2 B

:

¡

/

"

Base

(

A

)

A

^

/

"

Base

(

B

)

B

, X

/

A ^ Y

/

B , X

[

FCD

B

]

Y

.

Thus

X

[(

FCD

)(

RLD

B

)]

Y , X

[

FCD

B

]

Y

.

Proposition 8.10.

dom

(

FCD

)

f

=

dom

f

and im

(

FCD

)

f

=

im

f

for every reloid

f

.

Proof.

im

(

FCD

)

f

=

h

(

FCD

)

f

i

1

F

(

Src

f

)

=

d

f"

Dst

f

h

F

i

(

Src

f

)

j

F

2

GR

f

g

=

d

f"

Dst

f

im

F

j

F

2

GR

f

g

=

d

h"

Dst

f

ih

im

i

GR

f

=

im

f

.

dom

(

FCD

)

f

=

dom

f

is similar.

Proposition 8.11.

(

FCD

)(

f

u

(

RLD

B

)) = (

FCD

)

f

u

(

FCD

B

)

for every reloid

f

and

A 2

F

(

Src

f

)

and

B 2

F

(

Dst

f

)

.

Proof.

(

FCD

)(

f

u

(

RLD

B

)) = (

FCD

)(

id

B

RLD

f

id

A

RLD

) = (

FCD

)

id

B

RLD

(

FCD

)

f

(

FCD

)

id

A

RLD

=

id

B

FCD

(

FCD

)

f

id

A

FCD

= (

FCD

)

f

u

(

FCD

B

)

.

Corollary 8.12.

(

FCD

)(

f

j

A

) = ((

FCD

)

f

)

j

A

for every reloid

f

and a lter

A 2

F

(

Src

f

)

.

8.1 Funcoid induced by a reloid

133