17.14. ON PRODUCTS AND PROJECTIONS

272

So the value of

x

can be restored from

Q

(

C

)

x

by this formula.

17.14.3. Subatomic product.

Proposition

1400

.

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

1401

.

For every funcoid

f

:

Q

A

Q

B

(where

A

and

B

are

indexed families of sets) consider the funcoid Pr

(

A

)

k

f

defined by the formula

X

"

(

A

)

Pr

k

f

#

Y

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

X

if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

.

Proposition

1402

.

Pr

(

A

)

k

f

is really a funcoid.

Proof.

¬

h

Pr

(

A

)

k

f

i

Y

is obvious.

I

J

"

(

A

)

Pr

k

f

#

Y

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

(

I

J

) if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

I

t ↑

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

I

if

i

=

k

t

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

I

if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

F

(

B

i

)

if

i

6

=

k

;

B

i

Y

if

i

=

k

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

A

i

J

if

i

=

k

[

f

]

RLD

Y

i

dom

B

1

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

1403

.

For every funcoid

f

:

Q

A

Q

B

(where

A

and

B

are

indexed families of sets) there exists a 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

;

X

if

i

=

k

[

f

]

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

Y

if

i

=

k

.