21.13. ON PRODUCTS AND PROJECTIONS

356

So the value of

x

can be restored from

Q

(

C

)

x

by this formula.

21.13.3. Subatomic product.

Proposition

1798

.

Values

x

i

(for every

i

dom

x

) can be restored from the

value of

Q

(

A

)

x

provided that

x

is an indexed family of non-zero funcoids.

Proof.

Fix

k

dom

f

. Let for some filters

X

and

Y

a

=

>

F

(Base(

x

))

if

i

6

=

k

;

X

if

i

=

k

and

b

=

>

F

(Base(

y

))

if

i

6

=

k

;

Y

if

i

=

k.

Then

X

[

x

k

]

Y ⇔

a

k

[

x

k

]

b

k

⇔ ∀

i

dom

f

:

a

i

[

x

i

]

b

i

Q

RLD

a

h

Q

(

A

)

x

i

Q

RLD

b

.

So we have restored

x

k

from

Q

(

A

)

x

.

Definition

1799

.

For every funcoid

f

:

Q

A

Q

B

(where

A

and

B

are

indexed families of typed sets) consider the funcoid Pr

(

A

)

k

f

defined by the formula

X

"

(

A

)

Pr

k

f

#

Y

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

X

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

.

Proposition

1800

.

Pr

(

A

)

k

f

is really a funcoid.

Proof.

¬

h

Pr

(

A

)

k

f

i

Y

is obvious.

I

t

J

"

(

A

)

Pr

k

f

#

Y

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

(

I

t

J

) if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

I

t ↑

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

I

if

i

=

k

t

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

I

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

I

"

(

A

)

Pr

k

f

#

Y

J

"

(

A

)

Pr

k

f

#

Y.

The rest follows from symmetry.

Proposition

1801

.

For every funcoid

f

:

Q

A

Q

B

(where

A

and

B

are

indexed families of typed sets) the funcoid Pr

(

A

)

k

f

conforms to the formula

X

"

(

A

)

Pr

k

f

#

Y ⇔

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

X

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

Y

if

i

=

k

.