background image

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

∅ ⇒

GR StarComp

dom

x

;

Q

i

dom

x

Src

x

i

;

x

=

∅ ⇒

L

arity

a

y

Q

i

dom

x

Src

x

i

Q

i

dom

x

atoms Src

x

i

i

arity

a

:

y

i

[

x

i

]

L

i

L

arity

a

y

Q

i

dom

x

atoms Src

x

i

i

arity

a

:

y

i

[

x

i

]

L

i

⇔ ¬

i

arity

a

L

, y

atoms Src

x

i

:

y

[

x

i

]

L

⇒ ¬∀

i

arity

a

:

x

i

0

x

ZC

0

.

Thus

x

ZC

0

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

.

If

ρ

0

x

=

ρ

0

y

then arity

x

=

arity

y

=

n

for some index set

n

.

ρ

0

x

=

ρ

0

y

λi

n

: (

Src

x

=

Src

y

Dst

x

=

Dst

y

)

ρ

1

Q

(

C

)

x

=

FCD

(

StarHom

(

λi

dom

x

:

Src

x

i

);

StarHom

(

λi

dom

x

:

Dst

x

i

)) =

FCD

(

StarHom

(

λi

dom

y

:

Src

y

i

);

StarHom

(

λi

dom

y

:

Dst

y

i

)) =

ρ

1

Q

(

C

)

y

.

We have proved that it is a pre-quasi-cartesian function.

Next prove that it is a quasi-cartesian function, that is

 

Y

(

C

)

!

|

{

x

X

0

dom

A

|

ρ

0

x

=

A

}\

ZC

0

is an injection for every indexed family

A

of forms. Let

x

∈ {

x

X

0

dom

A

|

ρ

0

x

=

A

} \

ZC

0

. To

prove that it is an injection we will restore the value of

x

from

Q

(

C

)

x

.

D

Q

(

C

)

x

E

p

=

StarComp

(

p

;

x

)

for every

p

Q

i

n

atoms Src

x

i

.

It is easy to see that GR

p

Q

i

n

atoms Src

x

i

=

{

p

}

. Thus

L

GR StarComp

(

p

;

x

)

⇔ ∀

i

n

:

p

i

[

x

i

]

L

i

⇔ ∀

i

n

:

L

i

∈ h

x

i

i

p

i

for every

L

Q

i

n

Src

x

i

.

Thus GR StarComp

(

p

;

x

) =

Q

i

n

h

x

i

i

p

i

.

Since

x

i

0

there exist

p

such that

h

x

i

i

p

i

0

. Take

k

n

,

p

i

=

p

i

for

i

k

and

p

k

=

q

for an arbitrary

value

q

; then

h

x

k

i

q

=

Pr

k

Y

i

n

h

x

i

i

p

i

=

Pr

k

GR StarComp

(

p

;

x

) =

Pr

k

GR

*

Y

(

C

)

x

+

p

.

(2)

Note that the theorem ?? in [

?

applies to every

x

i

.

So the value of

x

can be restored from

Q

(

C

)

x

by this formula.

It remained to prove that it is with injective aggregation.

We have

Υ

F

= (

StarHom

(

λi

dom

f

:

F

i,

0

);

StarHom

(

λi

dom

f

:

F

i,

1

))

for every form

F

.

It is really an injection because StarHom

(

)

are disjoint.

Conjecture 38.

Cross-composition product (for small indexed families of reloids) is a quasi-

cartesian function (with injective aggregation) from the quasi-cartesian situation

S

0

of reloids to

the quasi-cartesian situation

S

1

of pointfree funcoids over posets with least elements.

Remark 39.

The above conjecture is unsolved even for product of two multipliers.

Theorem 40.

Reloidal product (for small indexed families of filters on powersets) with multireloid

projections is a product-projection system with injective aggregation from the quasi-cartesian situ-
ation

S

0

of filters to the quasi-cartesian situation

S

1

of multireloids.

10