 Proof

We will prove only the first as the second is similar. Let

f

=

Src

f

{

α

} ×

FCD

F

(

α

)

|

α

Src

f

=

Src

f

{

α

} ×

FCD

G

(

α

)

|

α

Src

f

for some

F, G

F

(Dst

f

)

Src

f

. We need to prove

F

=

G

. Let

β

Src

f

.

h

f

i {

β

}

=

Src

f

{

α

} ×

FCD

F

(

α

)

{

β

}

|

α

Src

f

=

F

(

β

)

.

Similarly

h

f

i {

β

}

=

G

(

β

). So

F

(

β

) =

G

(

β

).

3.12

Completion of funcoids

Theorem 34

Cor

f

= Cor

f

for an element

f

of a filtrator of funcoids. (Core

part is taken for the shifted filtrator of funcoids.)

Proof

From the theorem 26 in  and the corollary 10 and theorem 30.

Definition 35

Completion

of a funcoid

f

FCD

(

A

;

B

)

is the complete fun-

coid

Compl

f

FCD

(

A

;

B

)

defined by the formula

h

Compl

f

i

{

α

}

=

h

f

i

{

α

}

for

α

Src

f

.

Definition 36

Co-completion

of a funcoid

f

is defined by the formula

CoCompl

f

= (Compl

f

1

)

1

.

Obvious 15.

Compl

f

f

and CoCompl

f

f

for every funcoid

f

.

Proposition 24

The filtrator

(

FCD

(

A

;

B

) ; Compl

FCD

(

A

;

B

))

is filtered.

Proof

Because the shifted filtrator (

FCD

(

A

;

B

) ;

P

(

A

×

B

) ;

FCD

(

A

;

B

)

) is fil-

tered.

Theorem 35

Compl

f

= Cor

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

= Cor

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

for every funcoid

f

FCD

(

A

;

B

)

.

Proof

Cor

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

= Cor

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

since (the

theorem 26 in ) the filtrator (

FCD

(

A

;

B

) ; Compl

FCD

(

A

;

B

)) is filtered and

with join closed core (the theorem 29).

Let

g

up

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

. Then

g

Compl

FCD

(

A

;

B

) and

g

f

. Thus

g

= Compl

g

Compl

f

.

Thus

g

up

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

:

g

Compl

f

.

Let

g

up

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

:

h

g

for some

h

Compl

FCD

(

A

;

B

).

Then

h

T

FCD

(

A

;

B

)

up

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

=

f

and consequently

h

=

Compl

h

Compl

f

.

Thus

Compl

f

=

\

Compl

FCD

(

A

;

B

)

up

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f

= Cor

(

FCD

(

A

;

B

);Compl

FCD

(

A

;

B

))

f.

34