 6.5. MORE ON COMPOSITION OF FUNCOIDS

107

6.5. More on composition of funcoids

Proposition

609

.

[

g

f

] = [

g

]

◦ h

f

i

=

g

1

1

[

f

] for every composable

funcoids

f

and

g

.

Proof.

For every

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

) we have

X

[

g

f

]

Y ⇔

Y u h

g

f

iX 6

=

F

(Dst

g

)

Y u h

g

ih

f

iX 6

=

F

(Dst

g

)

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

]

.

Corollary

610

.

[

f

] = [id

Dst

f

]

◦ h

f

i

for every funcoid

f

.

FiXme

: Identity fun-

coid is defined

below

.

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

611

.

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

=

F

(

C

)

y

u h

f

iX 6

=

F

(

B

)

)

y

atoms

F

(

B

)

: (

Z u h

g

i

y

6

=

F

(

C

)

y

v h

f

iX

)

Z u h

g

ih

f

iX 6

=

F

(

C

)

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

612

.

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.