6.2. BASIC DEFINITIONS

99

Proof.

Let

f, g

FCD

(

A

;

B

).

Obviously,

h

f

i

=

h

g

i ⇒

[

f

]=[

g

] and

f

1

=

g

1

[

f

]=[

g

]. So it’s enough to

prove that [

f

]=[

g

]

⇒ h

f

i

=

h

g

i

.

Provided that [

f

]=[

g

] we have

Y 6 h

f

iX ⇔ X

[

f

]

Y ⇔ X

[

g

]

Y ⇔ Y 6 h

g

iX

and consequently

h

f

iX

=

h

g

iX

for every

X ∈

F

(

A

),

Y ∈

F

(

B

) because a set of

filters is separable, thus

h

f

i

=

h

g

i

.

Proposition

579

.

h

f

i⊥

F

(Src

f

)

=

F

(Dst

f

)

for every funcoid

f

.

Proof.

Y 6 h

f

i⊥

F

(Src

f

)

=

F

(Src

f

)

6

f

1

Y ⇔

0

⇔ Y 6 ⊥

F

(Dst

f

)

. Thus

h

f

i⊥

F

(Src

f

)

=

F

(Dst

f

)

by separability of filters.

Proposition

580

.

h

f

i

(

I t J

) =

h

f

iI t h

f

iJ

for every funcoid

f

and

I

,

J ∈

F

(Src

f

).

Proof.

?

h

f

i

(

I t J

) =

Y ∈

F

Y 6 h

f

i

(

I t J

)

=

Y ∈

F

I t J 6 h

f

1

iY

=

Y ∈

F

I 6 h

f

1

iY ∨ J 6 h

f

1

iY

=

Y ∈

F

Y 6 h

f

iI ∨ Y 6 h

f

iJ

=

Y ∈

F

Y 6 h

f

iI t h

f

iJ

=

?

(

h

f

iI t h

f

iJ

)

.

Thus

h

f

i

(

I t J

) =

h

f

iI t h

f

iJ

because

F

(Dst

f

) is separable.

Proposition

581

.

For every

f

FCD

(

A

;

B

) for every sets

A

and

B

we have:

1

.

K

[

f

]

I t J ⇔ K

[

f

]

I ∨ K

[

f

]

J

for every

I

,

J ∈

F

(

B

),

K ∈

F

(

A

).

2

.

I t J

[

f

]

K ⇔ I

[

f

]

K ∨ J

[

f

]

K

for every

I

,

J ∈

F

(

A

),

K ∈

F

(

B

).

Proof.

1

.

K

[

f

]

I t J ⇔

(

I t J

)

u h

f

iK 6

=

F

(

B

)

I u h

f

iK 6

=

F

(

B

)

∨ J u h

f

iK 6

=

F

(

B

)

K

[

f

]

I ∨ K

[

f

]

J

.

2

Similar.

6.2.1. Composition of funcoids.

Definition

582

.

Funcoids

f

and

g

are

composable

when Dst

f

= Src

g

.

Definition

583

.

Composition

of composable funcoids is defined by the formula

(

B

;

C

;

α

2

;

β

2

)

(

A

;

B

;

α

1

;

β

1

) = (

A

;

C

;

α

2

α

1

;

β

1

β

2

)

.

Proposition

584

.

If

f

,

g

are composable funcoids then

g

f

is a funcoid.