The reverse is obvious.

Corollary 6.66.

Let

f

be a funcoid.

The value of

f

can be restored knowing

h

f

ij

atoms

F

(

Src

f

)

.

The value of

f

can be restored knowing

[

f

]

j

atoms

F

(

Src

f

)

atoms

F

(

Dst

f

)

.

Theorem 6.67.

Let

A

and

B

be sets.

1. A function

2

F

(

B

)

atoms

F

(

A

)

such that (for every

a

2

atoms

F

(

A

)

)

a

v

l

G

h

atoms

"

A

a

(6.6)

can be continued to the function

h

f

i

for a unique

f

2

FCD

(

A

;

B

)

;

h

f

iX

=

G

h

i

atoms

X

(6.7)

for every

X 2

F

(

A

)

.

2. A relation

2

P

¡

atoms

F

(

A

)

atoms

F

(

B

)

such that (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

)

a  b

(6.8)

can be continued to the relation

[

f

]

for a unique

f

2

FCD

(

A

;

B

)

;

X

[

f

]

Y , 9

x

2

atoms

X

; y

2

atoms

Y

:

x  y

(6.9)

for every

X 2

F

(

A

)

,

Y 2

F

(

B

)

.

Proof.

Existence of no more than one such funcoids and formulas (

6.7

and (

6.9

follow from the

previous theorem.

1. Consider the function

0

2

F

(

B

)

P

A

dened by the formula (for every

X

2

P

A

)

0

X

=

G

h

i

atoms

"

A

X:

Obviously

0

;

= 0

F

(

B

)

. For every

I ; J

2

P

A

0

(

I

[

J

) =

G

h

i

atoms

"

A

(

I

[

J

)

=

G

h

i

(

atoms

"

A

I

[

atoms

"

A

J

)

=

G

(

h

i

atoms

"

A

I

[ h

i

atoms

"

A

J

)

=

G

h

i

atoms

"

A

I

t

G

h

i

atoms

"

A

J

=

0

I

t

0

J:

Let continue

0

till a funcoid

f

(by the theorem

6.28

):

h

f

iX

=

d

h

0

iX

.

Let's prove the reverse of (

6.6

):

l

G

h

atoms

"

A

a

=

l

G

h

i

h

atoms

ih"

A

i

a

v

l

G

h

i

ff

a

gg

=

l

¡G

h

i

f

a

g

=

l

G

h

if

a

g

=

l

G

f

a

g

=

l

f

a

g

=

a:

Finally,

a

=

l

G

h

atoms

"

A

a

=

l

h

0

i

a

=

h

f

i

a;

so

h

f

i

is a continuation of

.

2. Consider the relation

0

2

P

(

P

A

P

B

)

dened by the formula (for every

X

2

P

A

,

Y

2

P

B

)

0

Y

, 9

x

2

atoms

"

A

X ; y

2

atoms

"

B

Y

:

x  y:

Obviously

:

(

0

;

)

and

:

(

;

0

Y

)

.

6.8 Specifying funcoids by functions or relations on atomic filters

105