For suitable

I

and

J

we have:

I

[

0

Y

, 9

x

2

atoms

"

A

(

I

[

J

)

; y

2

atoms

"

B

Y

:

x  y

, 9

x

2

atoms

"

A

I

[

atoms

"

B

J ; y

2

atoms

"

B

Y

:

x  y

, 9

x

2

atoms

"

A

I ; y

2

atoms

"

B

Y

:

x  y

_ 9

x

2

atoms

"

A

J ; y

2

atoms

"

B

Y

:

x  y

,

0

Y

_

0

Y

;

similarly

0

I

[

J

,

0

I

_

0

J

for suitable

I

and

J

. Let's continue

0

till a funcoid

f

(by the

theorem

6.28

):

X

[

f

]

Y , 8

X

2 X

; Y

2 Y

:

0

Y :

The reverse of (

6.8

implication is trivial, so

8

X

2

a; Y

2

b

9

x

2

atoms

"

A

X ; y

2

atoms

"

B

Y

:

x  y

,

a  b:

8

X

2

a; Y

2

b

9

x

2

atoms

"

A

X ; y

2

atoms

"

B

Y

:

x  y

, 8

X

2

a; Y

2

b

:

0

Y

,

a

[

f

]

b

.

So

a  b

,

a

[

f

]

b

, that is

[

f

]

is a continuation of

.

One of uses of the previous theorem is the proof of the following theorem:

Theorem 6.68.

If

A

and

B

are sets,

R

2

P

FCD

(

A

;

B

)

,

x

2

atoms

F

(

A

)

,

y

2

atoms

F

(

B

)

, then

1.

h

d

R

i

x

=

d

fh

f

i

x

j

f

2

R

g

;

2.

x

[

d

R

]

y

, 8

f

2

R

:

x

[

f

]

y

.

Proof.

2. Let denote

x  y

, 8

f

2

R

:

x

[

f

]

y

. For every

a

2

atoms

F

(

A

)

,

b

2

atoms

F

(

B

)

8

X

2

a; Y

2

b

9

x

2

atoms

"

A

X ; y

2

atoms

"

B

Y

:

x  y

)

8

f

2

R; X

2

a; Y

2

b

9

x

2

atoms

"

A

X ; y

2

atoms

"

B

Y

:

x

[

f

]

y

)

8

f

2

R; X

2

a; Y

2

b

:

X

[

f

]

Y

)

8

f

2

R

:

a

[

f

]

b

,

a  b:

So by theorem

6.67

,

can be continued till

[

p

]

for some funcoid

p

2

FCD

(

A

;

B

)

.

For every funcoid

q

2

FCD

(

A

;

B

)

such that

8

f

2

R

:

q

v

f

we have

x

[

q

]

y

) 8

f

2

R

:

x

[

f

]

y

,

x  y

,

x

[

p

]

y

, so

q

v

p

. Consequently

p

=

d

R

.

From this

x

[

d

R

]

y

, 8

f

2

R

:

x

[

f

]

y

.

1. From the former

y

2

atoms

h

d

R

i

x

,

y

u h

d

R

i

x

=

/ 0

F

(

B

)

, 8

f

2

R

:

y

u h

f

i

x

=

/ 0

F

(

B

)

,

y

2

d

h

atoms

ifh

f

i

x

j

f

2

R

g ,

y

2

atoms

d

fh

f

i

x

j

f

2

R

g

for every

y

2

atoms

F

(

A

)

. From this it

follows

h

d

R

i

x

=

d

fh

f

i

x

j

f

2

R

g

.

Theorem 6.69.

g

f

=

d

f

G

F

j

F

2

up

f ; G

2

up

g

g

for every composable funcoids

f

and

g

.

Proof.

Let

x

2

atoms

F

(

Src

f

)

. Then

h

g

f

i

x

=

h

g

ih

f

i

x

=

(theorem

6.35

)

l

fh

G

ih

f

i

x

j

G

2

up

g

g

=

(theorem

6.35

)

l

h

G

i

l

fh

F

i

x

j

F

2

up

f

g j

G

2

up

g

=

(theorem

6.32

)

l

l

fh

G

ih

F

i

x

j

F

2

up

f

g j

G

2

up

g

=

l

fh

G

ih

F

i

x

j

F

2

up

f ; G

2

up

g

g

=

l

fh

G

F

i

x

j

F

2

up

f ; G

2

up

g

g

=

(theorem

6.68

)

l

f

G

F

j

F

2

up

f ; G

2

up

g

g

x:

Thus

g

f

=

d

f

G

F

j

F

2

up

f ; G

2

up

g

g

.

Theorem 6.70.

Let

A

,

B

,

C

be sets,

f

2

FCD

(

A

;

B

)

,

g

2

FCD

(

B

;

C

)

,

h

2

FCD

(

A

;

C

)

. Then

g

f

/

h

,

g

/

h

f

¡

1

:

106

Funcoids