 7.3. FUNCOID AS CONTINUATION

149

I

[

f

]

⊥ ⇔ ⊥ 6 h

f

i ↑

I

0;

I

t

J

[

f

]

K

(

I

t

J

) [

f

]

K

K

6 h

f

i ↑

(

I

t

J

)

K

6 h

f

i

(

I

t

J

)

K

6 h

f

i

I

t h

f

i

J

K

6 h

f

i

I

∨ ↑

K

6 h

f

i

J

I

[

f

]

K

J

[

f

]

K.

The rest follows from symmetry.

Theorem

828

.

(fundamental theorem of theory of funcoids) Fix sets

A

and

B

. Let

L

F

=

λf

FCD

(

A, B

) :

h

f

i

and

L

R

=

λf

FCD

(

A, B

) : [

f

]

.

1

.

L

F

is a bijection from the set

FCD

(

A, B

) to the set of functions

α

F

(

B

)

T

A

that obey the conditions (for every

I, J

T

A

)

α

=

,

α

(

I

t

J

) =

αI

t

αJ.

(5)

For such

α

it holds (for every

X ∈

F

(

A

))

L

1

F

α

X

=

l

h

α

i

up

X

.

(6)

2

.

L

R

is a bijection from the set

FCD

(

A, B

) to the set of binary relations

δ

P

(

T

A

×

T

B

) that obey the conditions

¬

(

I δ

)

,

I

t

J δ K

I δ K

J δ K

(for every

I, J

T

A

,

K

T

B

)

,

¬

(

δ I

)

,

K δ I

t

J

K δ I

K δ J

(for every

I, J

T

B

,

K

T

A

)

.

(7)

For such

δ

it holds (for every

X ∈

F

(

A

),

Y ∈

F

(

B

))

X

L

1

R

δ

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X δ Y.

(8)

Proof.

Injectivity of

L

F

and

L

R

, formulas (

6

(for

α

im

L

F

) and (

8

(for

δ

im

L

R

), formulas (

5

and (

7

follow from two previous theorems. The only

thing remaining to prove is that for every

α

and

δ

that obey the above conditions

a corresponding funcoid

f

exists.

2

Let define

α

F

(

B

)

T

A

by the formula

(

αX

) =

Y

T

B

XδY

for every

X

T

A

. (It is obvious that

Y

T

B

XδY

is a free star.) Analogously it can be

defined

β

F

(

A

)

T

B

by the formula

(

βY

) =

X

T

A

XδY

. Let’s continue

α

and

β

to

α

0

F

(

B

)

F

(

A

)

and

β

0

F

(

A

)

F

(

B

)

by the formulas

α

0

X

=

l

h

α

i

up

X

and

β

0

Y

=

l

h

β

i

up

Y

and

δ

to

δ

0

by the formula

X

δ

0

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X δ Y.

Y u

α

0

X 6

=

⊥ ⇔ Y u

d

h

α

i

up

X 6

=

⊥ ⇔

d

hYui

h

α

i

up

X 6

=

. Let’s prove

that

W

=

hYui

h

α

i

up

X

is a generalized filter base: To prove it is enough to show that

h

α

i

up

X

is a

generalized filter base. If

A

,

B ∈ h

α

i

up

X

then exist

X

1

, X

2

up

X

such that

A

=

αX

1

,

B

=

αX

2

.

Then

α

(

X

1

u

X

2

)

∈ h

α

i

up

X

. So

h

α

i

up

X

is a generalized filter base and

thus

W

is a generalized filter base.

By properties of generalized filter bases,

d

hYui

h

α

i

X 6

=

is equivalent to

X

up

X

:

Y u

αX

6

=

,