 17.15. RELATIONSHIPS BETWEEN CROSS-COMPOSITION AND SUBATOMIC PRODUCTS

273

Proof.

X

"

(

A

)

Pr

k

f

#

Y ⇔

X

∈ X

, Y

∈ Y

:

X

"

(

A

)

Pr

k

f

#

Y

X

∈ X

, Y

∈ 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

X

RLD

Y

i

dom

A

1

F

(

A

i

)

if

i

6

=

k

;

X

if

i

=

k

, Y

RLD

Y

i

dom

B

1

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

1404

.

Reloidal product above can be replaced with starred reloidal

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

Obvious

1405

.

Pr

(

A

)

k

Q

(

A

)

x

=

x

k

provided that

x

is an indexed family of

non-zero funcoids.

17.14.4. Other.

Conjecture

1406

.

Values

x

i

(for every

i

dom

x

) can be restored from the

value of

Q

(

C

)

x

provided that

x

is an indexed family of non-zero reloids.

Definition

1407

.

Displaced product

Q

(

DP

)

f

=

Q

(

C

)

f

for every indexed

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

FCD

(StarMor(Src

f

); StarMor(Dst

f

));

FCD

P

Y

(Src

f

)

×

Y

(Dst

f

)

.

Remark

1408

.

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

Conjecture

1409

.

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

1410

.

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

1411

.

Pr

(

D

)

k

Q

(

D

)

F

=

F

k

for every indexed family

F

of non-

empty relations.

Proof.

Obvious.

Corollary

1412

.

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.

17.15. Relationships between cross-composition and subatomic

products

Proposition

1413

.

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

).