 6.9. FUNCOIDAL PRODUCT OF FILTERS

114

Theorem

636

.

g

f

=

d

n

G

F

F

up

f.G

up

g

o

for every composable funcoids

f

and

g

.

Proof.

Let

x

atoms

F

(Src

f

)

. Then

h

g

f

i

x

=

h

g

ih

f

i

x

= (theorem

602

)

l

h

G

ih

f

i

x

G

up

g

= (theorem

602

)

l

h

G

i

d

n

h

F

i

F

up

f

o

G

up

g

= (theorem

599

)

l

d

n

h

G

ih

F

i

F

up

f

o

G

up

g

=

l

h

G

ih

F

i

x

F

up

f, G

up

g

=

l

h

G

F

i

x

F

up

f, G

up

g

= (theorem

635

)

l

G

F

F

up

f.G

up

g

x.

Thus

g

f

=

d

n

G

F

F

up

f.G

up

g

o

.

Theorem

637

.

Let

A

,

B

,

C

be sets,

f

FCD

(

A

;

B

),

g

FCD

(

B

;

C

),

h

FCD

(

A

;

C

). Then

g

f

6

h

g

6

h

f

1

.

Proof.

g

f

6

h

a

atoms

F

(

A

)

, c

atoms

F

(

C

)

:

a

[(

g

f

)

u

h

]

c

a

atoms

F

(

A

)

, c

atoms

F

(

C

)

: (

a

[

g

f

]

c

a

[

h

]

c

)

a

atoms

F

(

A

)

, b

atoms

F

(

B

)

, c

atoms

F

(

C

)

: (

a

[

f

]

b

b

[

g

]

c

a

[

h

]

c

)

b

atoms

F

(

B

)

, c

atoms

F

(

C

)

: (

b

[

g

]

c

b

h

f

1

c

)

b

atoms

F

(

B

)

, c

atoms

F

(

C

)

:

b

g

u

(

h

f

1

)

c

g

6

h

f

1

.

6.9. Funcoidal product of filters

A generalization of Cartesian product of two sets is funcoidal product of two

filters:

Definition

638

.

Funcoidal product

of filters

A

and

B

is such a funcoid

A ×

FCD

B ∈

FCD

(Base(

A

); Base(

B

)) that for every

X ∈

Base(

A

),

Y ∈

Base(

B

)

X

A ×

FCD

B

Y ⇔ X 6 A ∧ Y 6 B

.