background image

ρ

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

n

.

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

n

.

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

}

.

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.

Theorem 37.

Cross-composition product (for small indexed families of pointfree funcoids between

separable atomic posets with least elements and atomistic posets) is a quasi-cartesian function
(with injective aggregation) from the quasi-cartesian situation

S

0

of pointfree funcoids over posets

with least elements to the quasi-cartesian situation

S

1

of pointfree funcoids over posets with least

elements.

Proof.

First prove that it is a pre-quasi-cartesian function. We need to show that for every small

indexed families

x

,

y

of pointfree funcoids:

1.

x

ZC

0

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

;

2.

ρ

0

x

=

ρ

0

y

ρ

1

Q

(

C

)

x

=

ρ

1

Q

(

C

)

y

;

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

Q

(

C

)

x

=

Z

1

(

FCD

(

StarHom

(

λi

dom

x

:

Src

x

i

);

StarHom

(

λi

dom

x

:

Dst

x

i

)))

Q

(

C

)

x

= 0

FCD

(

StarHom

(

λi

dom

x

:

Src

x

i

);

StarHom

(

λi

dom

x

:

Dst

x

i

))

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

D

Q

(

C

)

x

E

a

= 0

StarHom

(

λi

dom

x

:

Dst

x

i

)

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

StarComp

(

a

;

x

) = 0

StarHom

(

λi

dom

x

:

Dst

x

i

)

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

;

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

∅ ⇐

x

ZC

0

.

9