Since

x

i

is non-zero there exist

p

such that

h

x

i

i

p

i

is non-zero. Take

k

2

n

,

p

i

0

=

p

i

for

i

=

/

k

and

p

k

0

=

q

for an arbitrary value

q

; then (using the staroidal projections from the previous subsection)

h

x

k

i

q

=

Pr

k

Strd

Y

i

2

n

Strd

h

x

i

i

p

i

0

=

Pr

k

Strd

*

Y

(

C

)

x

+

Y

Strd

p

0

:

So the value of

x

can be restored from

Q

(

C

)

x

by this formula.

17.14.3 Subatomic product

Proposition 17.203.

Values

x

i

(for every

i

2

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

2

dom

f

. Let for some lters

x

and

y

a

=

(

1

F

(

Base

(

x

))

if

i

=

/

k

;

x

if

i

=

k

and

b

=

(

1

F

(

Base

(

y

))

if

i

=

/

k

;

y

if

i

=

k:

Then

x

[

x

k

]

y

,

a

k

[

x

k

]

b

k

, 8

i

2

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

.

Denition 17.204.

For every funcoid

f

:

Q

A

!

Q

B

(where

A

and

B

are indexed families of

sets) consider the funcoid Pr

k

(

A

)

f

dened by the formula

X

h

Pr

k

(

A

)

f

i

Y

,

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

X

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

:

Proposition 17.205.

Pr

k

(

A

)

f

is really a funcoid.

Proof.

:

;

h

Pr

k

(

A

)

f

i

Y

is obvious.

I

[

J

h

Pr

k

(

A

)

f

i

Y

,

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

(

I

[

J

)

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

,

Y

i

2

domA

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

I

t "

A

i

J

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

,

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

I

if

i

=

k

!

t

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

J

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

,

Y

i

2

domA

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

I

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

_

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

"

A

i

J

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

"

B

i

Y

if

i

=

k

!

,

I

h

Pr

k

(

A

)

f

i

Y

_

J

h

Pr

k

(

A

)

f

i

Y :

The rest follows from symmetry.

Proposition 17.206.

For every funcoid

f

:

Q

A

!

Q

B

(where

A

and

B

are indexed families of

sets) there exists a funcoid Pr

k

(

A

)

f

dened by the formula

X

h

Pr

k

(

A

)

f

i

Y ,

Y

i

2

dom

A

RLD

(

1

F

(

A

i

)

if

i

=

/

k

;

X

if

i

=

k

!

[

f

]

Y

i

2

dom

B

RLD

(

1

F

(

B

i

)

if

i

=

/

k

;

Y

if

i

=

k

!

:

17.14 On products and projections

233