 Proof.

From the previous.

Remark 3.100.

Note that the above formulas contain both

S

i

2

dom

F

dom

F

i

0

and

S

i

2

dom

F

F

i

0

.

These forms are similar but dierent.

3.8.4.7 Associativity of ordinated product

Let

f

be an ordinal variadic function.

Let

S

be an ordinal indexed family of functions of ordinal indexed families of functions each

taking an ordinal number of arguments in a set

X

.

I call

f

innite associative

when

1.

f

(

f

S

) =

f

(

concat

S

)

for every

S

;

2.

f

(

J

x

K

) =

x

for

x

2

X

.

Innite associativity implies associativity

Proposition 3.101.

Let

f

be an innitely associative function taking an ordinal number of

arguments in a set

X

. Dene

x ? y

=

f

J

x

;

y

K

for

x; y

2

X

. Then the binary operation

?

is associative.

Proof.

Let

x; y; z

2

X

. Then

(

x ? y

)

? z

=

f

J

f

J

x

;

y

K

;

z

K

=

f

(

f

J

x

;

y

K

;

f

J

z

K

) =

f

J

x

;

y

;

z

K

. Similarly

x ?

(

y ? z

) =

f

J

x

;

y

;

z

K

. So

(

x ? y

)

? z

=

x ?

(

y ? z

)

.

Concatenation is associative

First we will prove some lemmas.
Let

a

and

b

be functions on a poset. Let

a

b

i there exist an order isomorphism

f

such that

a

=

b

f

. Evidently

is an equivalence relation.

Obvious 3.102.

concat

a

=

concat

b

,

uncurry

(

a

)

uncurry

(

b

)

for every ordinal indexed families

a

and

b

of functions taking an ordinal number of arguments.

Thank to the above, we can reduce properties of concat to properties of uncurry.

Lemma 3.103.

a

b

)

uncurry

a

uncurry

b

for every ordinal indexed families

a

and

b

of functions

taking an ordinal number of arguments.

Proof.

There exist an order isomorphism

f

such that

a

=

b

f

.

uncurry

(

a

)(

x

;

y

) = (

ax

)

y

= (

bfx

)

y

=

uncurry

(

b

)(

fx

;

y

) =

uncurry

(

b

)

g

(

x

;

y

)

where

g

(

x

;

y

) = (

fx

;

y

)

.

g

is an order isomorphism because

g

(

x

0

;

y

0

)

>

g

(

x

1

;

y

1

)

,

(

x

0

;

y

0

)

>

(

x

1

;

y

1

)

. (Injectivity and

surjectivity are obvious.)

Lemma 3.104.

Let

a

i

b

i

for some

f

i

for every

i

. Then uncurry

a

uncurry

b

for every ordinal

indexed families

a

and

b

of ordinal indexed families of functions taking an ordinal number of

arguments.

Proof.

Let

a

i

=

b

i

f

i

where

f

i

is an order isomorphism for every

i

.

uncurry

(

a

)(

i

;

y

) =

a

i

y

=

b

i

f

i

y

=

uncurry

(

b

)(

i

;

f

i

y

) =

uncurry

(

b

)

g

(

i

;

y

) = (

uncurry

(

b

)

g

)(

i

;

y

)

where

g

(

i

;

y

) = (

i

;

f

i

y

)

.

g

is an order isomorphism because

g

(

i

;

y

0

)

>

g

(

i

;

y

1

)

,

f

i

y

0

>

f

i

y

1

,

y

0

>

y

1

and

i

0

> i

1

)

g

(

i

0

;

y

0

)

> g

(

i

1

;

y

1

)

. (Injectivity and surjectivity are obvious.)

Let now

S

be an ordinal indexed family of ordinal indexed families of functions taking an ordinal

number of arguments.

Lemma 3.105.

uncurry

(

uncurry

S

)

uncurry

(

uncurry

S

)

.

Proof.

uncurry

S

=

i

2

S

:

uncurry

(

S

i

)

;

uncurry

(

uncurry

S

)(

i

; (

x

;

y

)) = (

uncurry

S

i

)(

x

;

y

) = (

S

i

x

)

y

;

(

uncurry

(

uncurry

S

))((

i

;

x

);

y

) = ((

uncurry

S

)(

i

;

x

))

y

= (

S

i

x

)

y

.

48

More on order theory