1. THE REST

38

Proof.

RLD

Y

i

n

h

CoCompl

f

i

iX

i

=

RLD

Y

i

n

Cor

h

f

i

iX

i

=

Cor

RLD

Y

i

n

h

f

i

iX

i

=

(*)

Cor

RLD

Y

i

n

h

f

i

i

RLD

Pr

i

RLD

Y

X

!

=

Cor

*

(

A

)

Y

f

+

RLD

Y

X

=

*

CoCompl

(

A

)

Y

f

+

RLD

Y

X

.

(*) You should verify the special case when

X

i

=

F

for some

i

.

Theorem

2098

.

Let

f

be an indexed family of funcoids.

FiXme

: Reverse

theorem (for non-least funcoids).

1

.

Q

f

is directly compact if every

f

i

is directly compact.

2

.

Q

f

is reversely compact if every

f

i

is reversely compact.

3

.

Q

f

is compact if every

f

i

is compact.

Proof.

It is enough to prove only the first statement.

Let each

f

i

is directly compact.

Let

h

Q

f

i

a

6

=

. Then

h

Q

f

i

a

=

D

Q

(

A

)

f

E

a

=

Q

RLD

i

dom

f

h

f

i

i

Pr

RLD

i

a

. Thus

every

h

f

i

i

Pr

RLD

i

a

6

=

.

Consequently by compactness Cor

h

f

i

i

Pr

RLD

i

a

6

=

;

Q

i

dom

f

Cor

h

f

i

i

Pr

RLD

i

a

6

=

; Cor

Q

i

dom

f

h

f

i

i

Pr

RLD

i

a

6

=

; Cor

h

Q

f

i

a

6

=

.

So

Q

f

is directly compact.

Proposition

2099

.

The following expressions are pairwise equal:

1

.

h

f

×

(

A

)

f

i

1

RLD

;

2

.

d

n

h

f

×

(

A

)

f

i

p

p

atoms 1

RLD

o

;

3

.

d

n

h

f

i

x

×

RLD

h

f

i

x

x

atoms

F

o

;

Proof.

1

2

Theorem 872.

2

3

.

d

n

h

f

×

(

A

)

f

i

p

p

atoms 1

RLD

o

=

d

n

h

f

i

dom

p

×

RLD

h

f

i

im

p

p

atoms 1

RLD

o

=

d

n

h

f

i

x

×

RLD

h

f

i

x

x

atoms

F

o

.

Proposition

2100

.

Let

g

be a reloid and

f

= (

FCD

)

g

and

f

=

f

f

1

. Then

h

f

×

(

A

)

f

i

1

RLD

w

g

.

Proof.

h

f

×

(

A

)

f

i

1

RLD

6↑

RLD

Y

⇔↑

RLD

1

RLD

[

f

×

(

A

)

f

]

RLD

Y

⇔↑

FCD

1

RLD

[

f

×

(

C

)

f

]

FCD

Y

f

◦ ↑

FCD

1

RLD

f

1

6↑

FCD

Y

f

f

1

6↑

FCD

Y

f

6↑

FCD

Y

f

u ↑

FCD

Y

6

=

⊥ ⇐

(

RLD

)

in

(

f

u ↑

FCD

Y

)

6

=

⊥ ⇔

(

RLD

)

in

f

u

(

RLD

)

in

FCD

Y

6

=

⊥ ⇐

(

RLD

)

in

f

u

(

RLD

)

out

FCD

Y

6

=

⊥ ⇔

(

RLD

)

in

f

u ↑

RLD

Y

6

=

⊥ ⇔

(

RLD

)

in

(

FCD

)

g

u ↑

RLD

Y

6

=

⊥ ⇐

g

u ↑

RLD

Y

6

=

⊥ ⇔

g

6↑

RLD

Y

.