background image

8.1. FUNCOID INDUCED BY A RELOID

150

Further

A

∈ A

, B

∈ B

:

X

h

FCD

(Base(

A

);Base(

B

))

(

A

×

B

)

i

Y ⇔

A

∈ A

, B

∈ B

: (

X 6↑

Base(

A

)

A

∧ Y 6↑

Base(

B

)

B

)

X 6 A ∧ Y 6 B ⇔ X

A ×

FCD

B

Y

.

Thus

X

(

FCD

)(

A ×

RLD

B

)

Y ⇔ X

A ×

FCD

B

Y

.

Proposition

808

.

dom(

FCD

)

f

= dom

f

and im(

FCD

)

f

= im

f

for every

reloid

f

.

Proof.

im(

FCD

)

f

=

h

(

FCD

)

f

i>

F

(Src

f

)

=

l

Dst

f

h

F

i

(Src

f

)

F

GR

f

=

l

Dst

f

im

F

F

GR

f

=

l

Dst

f

h

im

i

GR

f

= im

f.

dom(

FCD

)

f

= dom

f

is similar.

Proposition

809

.

(

FCD

)(

f

u

(

A ×

RLD

B

)) = (

FCD

)

f

u

(

A ×

FCD

B

) for every

reloid

f

and

A ∈

F

(Src

f

) and

B ∈

F

(Dst

f

).

Proof.

(

FCD

)(

f

u

(

A ×

RLD

B

)) =

(

FCD

)(id

RLD

B

f

id

RLD

A

) =

(

FCD

) id

RLD

B

(

FCD

)

f

(

FCD

) id

RLD

A

=

id

FCD

B

(

FCD

)

f

id

FCD

A

=

(

FCD

)

f

u

(

A ×

FCD

B

)

.

Corollary

810

.

(

FCD

)(

f

|

A

) = ((

FCD

)

f

)

|

A

for every reloid

f

and a filter

A ∈

F

(Src

f

).

Proposition

811

.

h

(

FCD

)

f

iX

= im(

f

|

X

) for every reloid

f

and a filter

X ∈

F

(Src

f

).

Proof.

im(

f

|

X

) = im(

FCD

)(

f

|

X

) = im(((

FCD

)

f

)

|

X

) =

h

(

FCD

)

f

iX

.

Proposition

812

.

(

FCD

)

f

=

F

n

x

×

FCD

y

x

atoms

F

(Src

f

)

,y

atoms

F

(Dst

f

)

,x

×

RLD

y

6

f

o

for ev-

ery reloid

f

.

Proof.

(

FCD

)

f

=

F

n

x

×

FCD

y

x

atoms

F

(Src

f

)

,y

atoms

F

(Dst

f

)

,x

×

FCD

y

6

(

FCD

)

f

o

, but

x

×

FCD

y

6

(

FCD

)

f

x

[(

FCD

)

f

]

y

x

×

RLD

y

6

f

, thus follows the theorem.