7.6. MORE ON COMPOSITION OF FUNCOIDS

156

Proof.

For every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

g

) we have

X

[

g

f

]

Y ⇔

Y u h

g

f

iX 6

=

⊥ ⇔

Y u h

g

ih

f

iX 6

=

⊥ ⇔

h

f

iX

[

g

]

Y ⇔

X

([

g

]

◦ h

f

i

)

Y

and

[

g

f

] =

(

f

1

g

1

)

1

=

f

1

g

1

1

=

(

f

1

g

1

)

1

=

g

1

1

[

f

]

.

The following theorem is a variant for funcoids of the statement (which defines

compositions of relations) that

x

(

g

f

)

z

⇔ ∃

y

: (

x f y

y g z

) for every

x

and

z

and every binary relations

f

and

g

.

Theorem

852

.

For every sets

A

,

B

,

C

and

f

FCD

(

A, B

),

g

FCD

(

B, C

)

and

X ∈

F

(

A

),

Z ∈

F

(

C

)

X

[

g

f

]

Z ⇔ ∃

y

atoms

F

(

B

)

: (

X

[

f

]

y

y

[

g

]

Z

)

.

Proof.

y

atoms

F

(

B

)

: (

X

[

f

]

y

y

[

g

]

Z

)

y

atoms

F

(

B

)

: (

Z u h

g

i

y

6

=

⊥ ∧

y

u h

f

iX 6

=

)

y

atoms

F

(

B

)

: (

Z u h

g

i

y

6

=

⊥ ∧

y

v h

f

iX

)

Z u h

g

ih

f

iX 6

=

⊥ ⇔

X

[

g

f

]

Z

.

Reversely, if

X

[

g

f

]

Z

then

h

f

iX

[

g

]

Z

, consequently there exists

y

atoms

h

f

iX

such that

y

[

g

]

Z

; we have

X

[

f

]

y

.

Theorem

853

.

For every sets

A

,

B

,

C

1

.

f

(

g

t

h

) =

f

g

t

f

h

for

g, h

FCD

(

A, B

),

f

FCD

(

B, C

);

2

. (

g

t

h

)

f

=

g

f

t

h

f

for

g, h

FCD

(

B, C

),

f

FCD

(

A, B

).

Proof.

I will prove only the first equality because the other is analogous.

For every

X ∈

F

(

A

),

Z ∈

F

(

C

)

X

[

f

(

g

t

h

)]

Z ⇔

y

atoms

F

(

B

)

: (

X

[

g

t

h

]

y

y

[

f

]

Z

)

y

atoms

F

(

B

)

: ((

X

[

g

]

y

∨ X

[

h

]

y

)

y

[

f

]

Z

)

y

atoms

F

(

B

)

: ((

X

[

g

]

y

y

[

f

]

Z

)

(

X

[

h

]

y

y

[

f

]

Z

))

y

atoms

F

(

B

)

: (

X

[

g

]

y

y

[

f

]

Z

)

∨ ∃

y

atoms

F

(

B

)

: (

X

[

h

]

y

y

[

f

]

Z

)

X

[

f

g

]

Z ∨ X

[

f

h

]

Z ⇔

X

[

f

g

t

f

h

]

Z

.