21.13. ON PRODUCTS AND PROJECTIONS

354

RLD

Y

a

(

A

)

Y

f

RLD

Y

b

x

atoms

RLD

Y

a, y

atoms

RLD

Y

b

:

x

(

A

)

Y

f

y

x

atoms

RLD

Y

a, y

atoms

RLD

Y

b

i

dom

f

:

D

Pr

i

E

x

[

f

i

]

D

Pr

i

E

y

i

dom

f

x

atoms

a

i

, y

atoms

b

i

:

x

[

f

i

]

y

i

dom

f

:

a

i

[

f

i

]

b

i

.

Theorem

1788

.

D

Q

(

A

)

f

E

x

=

Q

RLD

i

dom

f

h

f

i

i

Pr

RLD

i

x

for an indexed family

f

of

funcoids and

x

atoms

RLD

(

λi

dom

f

:Src

f

i

)

for every

n

dom

f

.

Proof.

For every ultrafilter

y

F

Q

i

dom

f

Dst

f

i

we have:

y

6

RLD

Y

i

dom

f

h

f

i

i

RLD

Pr

i

x

i

dom

f

:

RLD

Pr

i

y

6 h

f

i

i

RLD

Pr

i

x

i

dom

f

:

RLD

Pr

i

x

[

f

i

]

RLD

Pr

i

y

x

(

A

)

Y

f

y

y

6

*

(

A

)

Y

f

+

x.

Thus

D

Q

(

A

)

f

E

x

=

Q

RLD

i

dom

f

h

f

i

i

Pr

RLD

i

x

.

Corollary

1789

.

h

f

×

(

A

)

g

i

x

=

h

f

i

(dom

x

)

×

RLD

h

g

i

(im

x

) for atomic

x

.

21.13. On products and projections

Conjecture

1790

.

For principal funcoids

Q

(

C

)

and

Q

(

A

)

coincide with the

conventional product of binary relations.

21.13.1. Staroidal product.

Let

f

be a staroid, whose form components are

boolean lattices.

Definition

1791

.

Staroidal projection

of a staroid

f

is the filter Pr

Strd

k

f

cor-

responding to the free star

(val

f

)

k

(

λi

(arity

f

)

\ {

k

}

:

>

(form

f

)

i

)

.

Proposition

1792

.

Pr

k

GR

Q

Strd

x

=

?x

k

if

x

is an indexed family of proper

filters, and

k

dom

x

.