So (

A

;

C

;

α

2

α

1

;

β

1

β

2

) is a funcoid.

Obvious 7.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable funcoids

f

and

g

.

Proposition 9

(

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 5

(

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

.

3.3

Funcoid as continuation

Let

f

is a funcoid.

Definition 22

h

f

i

is the function

P

(Src

f

)

F

(Dst

f

)

defined by the for-

mula

h

f

i

X

=

h

f

i ↑

Src

f

X.

Definition 23

[

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 8.

1.

h

f

i

=

h

f

i ◦ ↑

Src

f

;

2. [

f

]

=

Dst

f

1

[

f

]

◦ ↑

Src

f

.

Theorem 6

For every funcoid

f

and

X ∈

F

(Src

f

)

and

Y ∈

F

(Dst

f

)

1.

h

f

i X

=

h

f

i

up

X

;

2.

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X

[

f

]

Y

.

Proof

2.

X

[

f

]

Y ⇔ Y ∩ h

f

i X 6

= 0

F

(Dst

f

)

⇔ ∀

Y

up

Y

:

Dst

f

Y

∩ h

f

i X 6

=

0

F

(Dst

f

)

⇔ ∀

Y

up

Y

:

X

[

f

]

Dst

f

Y

.

Analogously

X

[

f

]

Y ⇔ ∀

X

up

X

:

Src

f

X

[

f

]

Y

. Combining these two

equivalences we get

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

Src

f

X

[

f

]

Dst

f

Y

⇔ ∀

X

up

X

, Y

up

Y

:

X

[

f

]

Y.

1.

Y ∩ h

f

i X 6

= 0

F

(Dst

f

)

⇔ X

[

f

]

Y ⇔ ∀

X

up

X

:

Src

f

X

[

f

]

Y ⇔ ∀

X

up

X

:

Y ∩ h

f

i

X

6

= 0

F

(Dst

f

)

.

12