 Theorem 6.28.

Fix sets

A

and

B

. Let

L

F

=

f

2

FCD

(

A

;

B

):

h

f

i

and

L

R

=

f

2

FCD

(

A

;

B

): [

f

]

.

1.

L

F

is a bijection from the set

FCD

(

A

;

B

)

to the set of functions

2

F

(

B

)

P

A

that obey the

conditions (for every

I ; J

2

P

A

)

;

= 0

F

(

B

)

;

(

I

[

J

) =

I

t

J:

(6.1)

For such

it holds (for every

X 2

F

(

A

)

)

h

L

F

¡

1

iX

=

l

h

iX

:

(6.2)

2.

L

R

is a bijection from the set

FCD

(

A

;

B

)

to the set of binary relations

2

P

(

P

A

P

B

)

that obey the conditions

:

(

;

)

; I

[

J  K

,

I  K

_

J  K

(for every

I ; J

2

P

A

,

K

2

P

B

)

;

:

(

;

I

)

; K  I

[

J

,

K  I

_

K  J

(for every

I ; J

2

P

B

,

K

2

P

A

).

(6.3)

For such

it holds (for every

X 2

F

(

A

)

,

Y 2

F

(

B

)

)

X

[

L

R

¡

1

]

Y , 8

X

2 X

; Y

2 Y

:

X  Y :

(6.4)

Proof.

Injectivity of

L

F

and

L

R

, formulas (

6.2

(for

2

im

L

F

) and (

6.4

(for

2

im

L

R

), formulas

(

6.1

and (

6.3

follow from two previous theorems. The only thing remained to prove is that for

every

and

that obey the above conditions a corresponding funcoid

f

exists.

2. Let dene

2

F

(

B

)

P

A

by the formula

@

(

X

) =

f

Y

2

P

B

j

X  Y

g

for every

X

2

P

A

. (It is

obvious that

f

Y

2

P

B

j

X  Y

g

is a free star.) Analogously it can be dened

2

F

(

A

)

P

B

by the

formula

@

(

Y

) =

f

X

2

P

A

j

X  Y

g

. Let's continue

and

to

0

2

F

(

B

)

F

(

A

)

and

0

2

F

(

A

)

F

(

B

)

by the formulas

0

X

=

l

h

iX

and

0

Y

=

l

h

iY

and

to

0

2

P

(

F

(

A

)

F

(

B

))

by the formula

X

0

Y , 8

X

2 X

; Y

2 Y

:

X  Y :

Y u

0

X

=

/ 0

F

(

B

)

, Y u

d

h

iX

=

/ 0

F

(

B

)

,

d

hY u ih

iX

=

/ 0

F

(

B

)

. Let's prove that

W

=

hY u ih

iX

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

h

iX

is a generalized lter base. If

A

;

B 2 h

iX

then exist

X

1

; X

2

2 X

such that

A

=

X

1

,

B

=

X

2

.

Then

(

X

1

\

X

2

)

2 h

iX

. So

h

iX

is a generalized lter base and thus

W

is a generalized lter

base.

By properties of generalized lter bases,

d

hY u ih

iX

=

/ 0

F

(

B

)

is equivalent to

8

X

2 X

:

Y u

X

=

/ 0

F

(

B

)

;

what is equivalent to

8

X

2 X

; Y

2 Y

:

"

B

Y

u

X

=

/ 0

F

(

B

)

, 8

X

2 X

; Y

2 Y

:

Y

2

@

(

X

)

, 8

X

2 X

;

Y

2 Y

:

X  Y

. Combining the equivalencies we get

Y u

0

X

=

/ 0

F

(

B

)

, X

0

Y

. Analogously

X u

0

Y

=

/ 0

F

(

A

)

, X

0

Y

. So

Y u

0

X

=

/ 0

F

(

B

)

, X u

0

Y

=

/ 0

F

(

A

)

, that is

(

A

;

B

;

0

;

0

)

is a funcoid.

From the formula

Y u

0

X

=

/ 0

F

(

B

)

, X

0

Y

it follows that

X

[(

A

;

B

;

0

;

0

)]

Y

, "

B

Y

u

0

"

A

X

=

/ 0

F

(

B

)

, "

A

0

"

B

Y

,

X  Y :

1. Let dene the relation

2

P

(

P

A

P

B

)

by the formula

X  Y

, "

B

Y

u

X

=

/ 0

F

(

B

)

.

That

:

(

;

)

and

:

(

;

I

)

is obvious. We have

I

[

J  K

, "

B

K

u

(

I

[

J

) =

/ 0

F

(

B

)

,

"

B

K

u

(

I

t

J

) =

/ 0

F

(

B

)

, "

B

K

u

I

=

/ 0

F

(

B

)

_ "

B

K

u

J

=

/ 0

F

(

B

)

,

I  K

_

J  K

and

K  I

[

J

, "

B

(

I

[

J

)

u

K

=

/ 0

F

(

B

)

,

(

"

B

I

t "

B

J

)

u

K

=

/ 0

F

(

B

)

, "

B

I

u

K

=

/ 0

F

(

B

)

_

"

B

J

u

K

=

/ 0

F

(

B

)

,

K  I

_

K  J

.

That is the formulas (

6.3

are true.

Accordingly to the above there exists a funcoid

f

such that

X

[

f

]

Y , 8

X

2 X

; Y

2 Y

:

X  Y :

6.3 Funcoid as continuation

99