 6.10. ATOMIC FUNCOIDS

119

2

.

atoms

f

t

l

R

=

atoms

f

atoms

l

R

=

atoms

f

\

h

atoms

i

R

=

\

h

(atoms

f

)

∪i

h

atoms

i

R

= (use the following equality)

\

h

atoms

i

h

f

ti

R

=

atoms

l

h

f

ti

R.

h

(atoms

f

)

∪i

h

atoms

i

R

=

(atoms

f

)

A

A

∈ h

atoms

i

R

=

(atoms

f

)

A

C

R

:

A

= atoms

C

=

(atoms

f

)

(atoms

C

)

C

R

=

atoms(

f

t

C

)

C

R

=

atoms

B

C

R

:

B

=

f

t

C

=

atoms

B

B

∈ h

f

ti

C

=

h

atoms

i

h

f

ti

R.

Note that distributivity of the lattice of funcoids is proved through using atoms

of this lattice. I have never seen such method of proving distributivity.

FiXme

:

Probably should remove this paragraph.

Corollary

658

.

The lattice

FCD

(

A

;

B

) is co-brouwerian (for every sets

A

,

B

).

Conjecture

659

.

Distributivity of the lattice

FCD

(

A

;

B

) of funcoids (for arbi-

trary sets

A

and M) is not provable in ZF (without axiom of choice).

FiXme

: Solved

by

Todd Trimble

?

The next proposition is one more (among the theorem

611

generalization for

funcoids of composition of relations.

Proposition

660

.

For every composable funcoids

f

,

g

atoms(

g

f

) =

x

×

FCD

z

x

atoms

F

(Src

f

)

, y

atoms

F

(Dst

g

)

,

y

atoms

F

(Dst

f

)

: (

x

×

FCD

y

atoms

f

y

×

FCD

z

atoms

g

)

.

Proof.

Using the theorem

611

,

x

×

FCD

z

6

g

f

x

[

g

f

]

z

⇔ ∃

y

atoms

F

(Dst

f

)

: (

x

×

FCD

y

6

f

y

×

FCD

z

6

g

)

.