background image

Proof.

X

h

Pr

k

(

A

)

f

i

Y ,

8

X

2 X

; Y

2 Y

:

X

h

Pr

k

(

A

)

f

i

Y

,

8

X

2 X

; Y

2 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

!

,

8

X

2

Y

i

2

dom

A

RLD

 (

1

F

(

A

i

)

if

i

=

/

k

;

X

if

i

=

k

!

; Y

2

Y

i

2

dom

B

RLD

 (

1

F

(

B

i

)

if

i

=

/

k

;

Y

if

i

=

k

!

:

X

[

f

]

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

!

:

Remark 17.207.

Reloidal product above can be replaced with starred reloidal product, because

of nite number of non-maximal multipliers in the products.

Obvious 17.208.

Pr

k

(

A

)

Q

(

A

)

x

=

x

k

provided that

x

is an indexed family of non-zero funcoids.

17.14.4 Other

Conjecture 17.209.

Values

x

i

(for every

i

2

dom

x

) can be restored from the value of

Q

(

C

)

x

provided that

x

is an indexed family of non-zero reloids.

Denition 17.210.

Displaced product

Q

(

DP

)

f

=

Q

(

C

)

f

for every indexed family of pointfree

funcoids, where downgrading is dened for the ltrator

¡

FCD

(

StarMor

(

Src

f

);

StarMor

(

Dst

f

));

h"

FCD

i

P

¡Y

(

Src

f

)

Y

(

Dst

f

)

:

Remark 17.211.

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

Conjecture 17.212.

Values

x

i

(for every

i

2

dom

x

) can be restored from the value of

Q

(

DP

)

x

provided that

x

is an indexed family of non-zero funcoids.

Denition 17.213.

Let

f

2

P

¡

Z

`

Y

where

Z

is a set and

Y

is a function.

Pr

k

(

D

)

f

=

Pr

k

f

curry

z

j

z

2

f

g

:

Proposition 17.214.

Pr

k

(

D

)

Q

(

D

)

F

=

F

k

for every indexed family

F

of non-empty relations.

Proof.

Obvious.

Corollary 17.215.

GR Pr

k

(

D

)

Q

(

D

)

F

=

GR

F

k

and form Pr

k

(

D

)

Q

(

D

)

F

=

form

F

k

for every indexed

family

F

of non-empty anchored relations.

17.15 Relationships between cross-composition and sub-

atomic products

Proposition 17.216.

a

f

(

C

)

g

b

,

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

for funcoids

f

and

g

and

atomic funcoids

a

2

FCD

(

Src

f

;

Src

g

)

and

b

2

FCD

(

Dst

f

;

Dst

g

)

.

Proof.

a

f

(

C

)

g

b

,

a

f

¡

1

/

g

¡

1

b

,

(

dom

a

FCD

im

a

)

f

¡

1

/

g

¡

1

(

dom

b

FCD

im

b

)

,

h

f

i

dom

a

FCD

im

a

/

dom

b

FCD

h

g

¡

1

i

im

b

, h

f

i

dom

a

/

dom

b

^

im

a

/

h

g

¡

1

i

im

b

,

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

.

234

Multifuncoids and staroids