Lemma 27.

n

f

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

=

S

im

P

|

P

Q

i

dom

F

F

i

.

Proof.

L

S

im

P

|

P

Q

i

dom

F

F

i

L

S

im

P

|

P

`

i

dom

F

{

i

arity

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

L

`

i

X

arity

F

i

curry

(

L

)

Q

(

GR

F

)

L

`

i

X

arity

F

i

curry

(

L

)

n

curry

(

f

)

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

(because

L

(

arity

F

)

is a

bijection)

curry

(

L

)

(

L

(

arity

F

))

1

n

curry

(

f

)

|

f

GR

Q

(

ord

)

F

o

L

(

L

(

arity

F

))

1

n

f

|

f

GR

Q

(

ord

)

F

o

(because

L

(

arity

F

)

is a bijection)

L

n

f

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

.

Theorem 28.

GR

Y

(

ord

)

F

=

(

[

im

P

M

(

arity

F

)

1

|

P

Y

i

dom

F

F

i

)

.

Proof.

From the lemma, because

L

(

arity

F

)

is a bijection.

Theorem 29.

GR

Y

(

ord

)

F

=

(

[

i

dom

F

P

i

M

(

arity

F

)

1

|

P

Y

i

dom

F

F

i

)

.

Proof.

From the previous theorem.

Theorem 30.

GR

Y

(

ord

)

F

=

(

[

im

P

|

P

Y

i

dom

F

f

M

(

arity

F

)

1

|

f

F

i

)

.

Proof.

From the previous.

Remark 31.

Note that the above formulas contain both

S

i

dom

F

dom

F

i

and

S

i

dom

F

F

i

. These

forms are similar but different.

4.7 Associativity of ordinated product

Let

f

is an ordinal variadic function.

Let

S

is 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

infinite associative

when

1.

f

(

f

S

) =

f

(

concat

S

)

for every

S

;

2.

f

(

J

x

K

) =

x

for

x

X

.

4.7.1 Infinite associativity impliess associativity

Proposition 32.

Let

f

is an infinitely associative function taking an ordinal number of arguments

in a set

X

. Define

x ⋆ y

=

f

J

x

;

y

K

for

x, y

X

. Then the binary operation

is associative.

Proof.

Let

x, y, z

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

)

.

4.7.2 Concatenation is associative

First we will prove some lemmas.

6

Section 4