6.3. FUNCOID AS CONTINUATION

100

Proof.

Let

f

= (

A

;

B

;

α

1

;

β

1

),

g

= (

B

;

C

;

α

2

;

β

2

). For every

X ∈

F

(

A

),

Y ∈

F

(

C

) we have

Y 6

(

α

2

α

1

)

X ⇔ Y 6

α

2

α

1

X ⇔

α

1

X 6

β

2

Y ⇔ X 6

β

1

β

2

Y ⇔ X 6

(

β

1

β

2

)

Y

.

So (

A

;

C

;

α

2

α

1

;

β

1

β

2

) is a funcoid.

Obvious

585

.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable funcoids

f

and

g

.

Proposition

586

.

(

h

g

)

f

=

h

(

g

f

) for every composable funcoids

f

,

g

,

h

.

Proof.

h

(

h

g

)

f

i

=

h

h

g

i ◦ h

f

i

=

(

h

h

i ◦ h

g

i

)

◦ h

f

i

=

h

h

i ◦

(

h

g

i ◦ h

f

i

) =

h

h

i ◦ h

g

f

i

=

h

h

(

g

f

)

i

.

Theorem

587

.

(

g

f

)

1

=

f

1

g

1

for every composable funcoids

f

and

g

.

Proof.

(

g

f

)

1

=

f

1

g

1

=

f

1

g

1

.

6.3. Funcoid as continuation

Let

f

be a funcoid.

FiXme

: Need to say explicitly that

h

f

i

and [

f

]

coincide

for funcoids and binary relations.

Definition

588

.

h

f

i

is the function

P

(Src

f

)

F

(Dst

f

) defined by the

formula

h

f

i

X

=

h

f

i ↑

Src

f

X.

Definition

589

.

[

f

]

is the relation between

P

(Src

f

) and

P

(Dst

f

)defined

by the formula

X

[

f

]

Y

⇔↑

Src

f

X

[

f

]

Dst

f

Y.

Obvious

590

.

1

.

h

f

i

=

h

f

i◦ ↑

Src

f

;

2

. [

f

]

= (

Dst

f

)

1

[

f

]

◦ ↑

Src

f

.

Obvious

591

.

h

g

ih

f

i

X

=

h

g

f

i

X

for every

X

P

(Src

f

).

Theorem

592

.

For every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)

1

.

h

f

iX

=

d

h

f

i

X

;

2

.

X

[

f

]

Y ⇔ ∀

X

∈ X

, Y

∈ Y

:

X

[

f

]

Y

.

Proof.

2

.

X

[

f

]

Y ⇔

Y u h

f

iX 6

=

F

(Dst

f

)

Y

∈ Y

:

Dst

f

Y

u h

f

iX 6

=

F

(Dst

f

)

Y

∈ Y

:

X

[

f

]

Dst

f

Y.