 21.14. CROSS-COMPOSITION AND SUBATOMIC PRODUCTS

357

Proof.

X

"

(

A

)

Pr

k

f

#

Y ⇔

X

up

X

, Y

up

Y

:

X

"

(

A

)

Pr

k

f

#

Y

X

up

X

, Y

up

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

X

up

RLD

Y

i

dom

A

>

F

(

A

i

)

if

i

6

=

k

;

X

if

i

=

k

, Y

up

RLD

Y

i

dom

B

>

F

(

B

i

)

if

i

6

=

k

;

Y

if

i

=

k

:

X

[

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

.

Remark

1802

.

Reloidal product above can be replaced with starred reloidal

product, because of finite number of non-maximal multipliers in the products.

Obvious

1803

.

Pr

(

A

)

k

Q

(

A

)

x

=

x

k

provided that

x

is an indexed family of

non-zero funcoids.

21.13.4. Other.

Definition

1804

.

Displaced product

Q

(

DP

)

f

=

Q

(

C

)

f

for every indexed

family of pointfree funcoids, where downgrading is defined for the filtrator

FCD

(StarHom(Src

f

)

,

StarHom(Dst

f

))

,

Rel

Y

(Src

f

)

,

Y

(Dst

f

)

.

Remark

1805

.

Displaced product is a funcoid (not just a pointfree funcoid).

Conjecture

1806

.

Values

x

i

(for every

i

dom

x

) can be restored from the

value of

Q

(

DP

)

x

provided that

x

is an indexed family of non-zero funcoids.

Definition

1807

.

Let

f

P

Z

`

Y

where

Z

is a set and

Y

is a function.

(

D

)

Pr

k

f

= Pr

k

curry

z

z

f

.

Proposition

1808

.

Pr

(

D

)

k

Q

(

D

)

F

=

F

k

for every indexed family

F

of non-

empty relations.

Proof.

Obvious.

Corollary

1809

.

GR Pr

(

D

)

k

Q

(

D

)

F

= GR

F

k

and form Pr

(

D

)

k

Q

(

D

)

F

=

form

F

k

for every indexed family

F

of non-empty anchored relations.

21.14. Relationships between cross-composition and subatomic

products

Proposition

1810

.

a

f

×

(

C

)

g

b

dom

a

[

f

] dom

b

im

a

[

g

] im

b

for fun-

coids

f

and

g

and atomic funcoids

a

FCD

(Src

f,

Src

g

) and

b

FCD

(Dst

f,

Dst

g

).