 Proposition 7.

`

a

with lexigraphic order is a well-ordered set.

Proof.

Let

S

is non-empty subset of

`

a

.

Take

i

0

=

inf Pr

0

S

and

x

0

=

inf

a

i

0

(these exist by properties of ordinals). Then

(

i

0

;

x

0

)

is the

least element of

S

.

Definition 8.

P

a

is the unique ordinal order-isomorphic to

`

a

.

This ordinal exists and is unique because our set is well-ordered.

Remark 9.

An infinite sum of ordinals is not customary defined.

The

structured sum

L

a

of

a

is an order isomorphism from lexigraphically ordered set

`

a

into

P

a

.

There exist (for a given

a

) exactly one structured sum, by properties of well-ordered sets.

Obvious 10.

P

a

=

im

L

a

.

Theorem 11.

(

L

a

)(

n

;

x

) =

P

i

n

a

i

+

x

.

Proof.

We need to prove that it is an order isomorphism. Let’s prove it is an injection that is

m > n

P

i

m

a

i

+

x >

P

i

n

a

i

+

x

and

y > x

P

i

n

a

i

+

y >

P

i

n

a

i

+

x

.

Really, if

m > n

then

P

i

m

a

i

+

x

>

P

i

n

+1

a

i

+

x >

P

i

n

a

i

+

x

. The second formula is true

by properties of ordinals.

Let’s prove that it is a surjection. Let

r

P

a

. There exist

n

dom

a

and

x

a

n

such that

r

= (

L

a

)(

n

;

x

)

. Thus

r

= (

L

a

)(

n

; 0) +

x

=

P

i

n

a

i

+

x

because

(

L

a

)(

n

; 0) =

P

i

n

a

i

since

(

n

; 0)

has

P

i

n

a

i

predecessors.

4 Ordinated product

4.1 Introduction

Ordinated product

defined below is a variation of cartesian product, but is associative unlike

cartesian product. However, ordinated product unlike cartesian product is defined not for arbitrary
sets, but only for relations having ordinal numbers of arguments.

Let

F

indexed by an ordinal number is a small family of anchored relations.

4.2 Concatenation

Definition 12.

Let

z

is an indexed by an ordinal number family of functions each taking an ordinal

number of arguments. The

concatenation

of

z

is

concat

z

=

uncurry

(

z

)

M

(

dom

z

)

1

.

Obvious 13.

If

z

is a finite family of finitary functions, it is concatenation of dom

z

tuples in the

usual sense (as it is commonly used in computer science).

Proposition 14.

If

z

Q

(

GR

F

)

then concat

z

=

uncurry

(

z

)

(

L

(

arity

F

))

1

.

Proof.

If

z

Q

(

GR

F

)

then dom

z

(

i

) =

dom

(

GR

F

)

i

=

dom

F

i

=

arity

F

i

for every

i

dom

F

.

Thus dom

z

=

arity

F

.

Proposition 15.

dom concat

z

=

P

i

dom

z

dom

z

i

.

Proof.

Because dom

(

L

(

dom

z

))

1

=

P

i

dom

F

dom

z

i

, it is enough to prove that

dom uncurry

(

z

) =

dom

M

(

dom

z

)

.

Ordinated product

3