 Ordered quasi-cartesian situations

Definition 41.

An ordered quasi-cartesian situation is a quasi-cartesian situation together with a

partial order on each its set of its arguments of each given form.

Definition 42.

An order-preserving quasi-cartesian function from a quasi-cartesian situation

S

0

to a quasi-cartesian situation

S

1

is a quasi-cartesian function

σ

such that

σx

σy

x

y

for

every indexed family

A

of forms and

x, y

∈ {

x

X

0

dom

A

|

ρ

0

x

=

A

} \

ZC

0

.

Obvious 43.

Every order-preserving quasi-cartesian function is a quasi-cartesian function with

injective aggregation.

Remark 44.

Using the obvious fact above, we can prove again that the considered quasi-cartesian

functions are with injective aggregation using the below proved statements that they are order-
preserving.

Proposition 45.

Cross-composition product (for small indexed families of relations) is an order-

preserving quasi-cartesian function from the quasi-cartesian situation

S

0

of binary relations to the

quasi-cartesian situation

S

1

of pointfree funcoids over posets with least elements equipped with the

usual orderings of these sets.

Proof.

We need to prove

i

n

: (

f

i

∅ ∧

g

i

)

Q

C

f

Q

C

g

f

g

for every

n

-indexed

families

f

and

g

of binary relations.

D

Q

(

C

)

f

E

Q

a

=

Q

i

n

h

f

i

i

a

i

.

Fix

k

n

,

x

. Let

a

=

n

\{

k

}

∪ {

(

k

;

x

)

}

. Then

*

Y

(

C

)

f

+

Y

a

=

Y

i

n

h

f

i

i

if

i

k

;

h

f

k

i{

x

}

if

i

=

k.

and

*

Y

(

C

)

g

+

Y

a

=

Y

i

n

h

g

i

i

if

i

k

;

h

g

k

i{

x

}

if

i

=

k.

Taking into account that

h

f

i

i

and

h

g

i

i

for every

i

n

, by properties of Cartesian product,

we get

h

f

k

i{

x

} ⊑ h

g

k

i{

x

}

for every

x

and thus

f

k

g

k

.

Corollary 46.

Cross-composition product (for small indexed families of

Rel

-morphisms) is an

order-preserving quasi-cartesian function from the quasi-cartesian situation

S

0

of

Rel

-morphisms

to the quasi-cartesian situation

S

1

of pointfree funcoids over posets with least elements.

Theorem 47.

Let each

A

i

(for

i

n

where

n

is some index set) is a separable poset with least

element. Then

i

n

:

a

i

0

Y

FCD

a

Y

FCD

b

a

b.

Proof.

Suppose

a

b

.

Q

A

is a separable poset, Thus it exists

y

a

such that

y

b

.

We have

i

n

:

y

i

a

i

and

i

n

:

y

i

b

i

.

Take

k

n

such that

y

k

a

k

. We have

y

k

b

k

.

Take

z

i

=

a

i

if

i

k

;

y

k

if

i

=

k

for

i

n

.

11