Lemma 3.94.

n

curry

(

f

)

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

=

Q

(

GR

F

)

.

Proof.

First GR

Q

(

ord

)

F

=

f

uncurry

(

z

)

(

L

(

dom

z

))

¡

1

j

z

2

Q

(

GR

F

)

g

, that is

n

f

j

f

2

GR

Q

(

ord

)

F

o

=

f

uncurry

(

z

)

(

L

(

arity

F

))

¡

1

j

z

2

Q

(

GR

F

)

g

.

Since

L

(

arity

F

)

is a bijection, we have

n

f

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

=

f

uncurry

(

z

)

j

z

2

Q

(

GR

F

)

g

what is equivalent to

n

curry

(

f

)

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

=

f

z

j

z

2

Q

(

GR

F

)

g

that is

n

curry

(

f

)

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

=

Q

(

GR

F

)

.

Lemma 3.95.

S

im

P

j

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

^

curry

(

S

im

P

)

2

Q

(

GR

F

)

=

n

L

2

f

`

i

2

dom

F

arity

F

i

j

curry

(

L

)

2

Q

(

GR

F

)

o

.

Proof.

Let

L

0

2

n

L

2

f

`

i

2

X

arity

F

i

j

curry

(

L

)

2

Q

(

GR

F

)

o

. Then

L

0

2

f

`

i

2

dom

F

arity

F

i

and

curry

(

L

0

)

2

Q

(

GR

F

)

.

Let

P

=

i

2

dom

F

:

L

0

j

f

i

g

arity

F

i

. Then

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

and

S

im

P

=

L

0

. So

L

0

2

S

im

P

j

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

^

curry

(

S

im

P

)

2

Q

(

GR

F

)

.

Let now

L

0

2

S

im

P

j

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

^

curry

(

S

im

P

)

2

Q

(

GR

F

)

. Then there

exists

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

such that

L

0

=

S

im

P

and curry

(

L

0

)

2

Q

(

GR

F

)

. Evidently

L

0

2

f

`

i

2

dom

F

arity

F

i

. So

L

0

2

S

im

P

j

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

^

curry

(

S

im

P

)

2

Q

(

GR

F

)

.

Lemma 3.96.

n

f

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

=

S

im

P

j

P

2

Q

i

2

dom

F

F

i

0

.

Proof.

L

2

S

im

P

j

P

2

Q

i

2

dom

F

F

i

0

,

L

2

S

im

P

j

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

^

curry

(

S

im

P

)

2

Q

(

GR

F

)

,

L

2

f

`

i

2

dom

F

arity

F

i

^

curry

(

L

)

2

Q

(

GR

F

)

,

L

2

f

`

i

2

dom

F

arity

F

i

^

curry

(

L

)

2

n

curry

(

f

)

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

,

(because

L

(

arity

F

)

is a bijection)

,

curry

(

L

)

(

L

(

arity

F

))

¡

1

2

n

curry

(

f

)

j

f

2

GR

Q

(

ord

)

F

o

,

L

(

L

(

arity

F

))

¡

1

2

n

f

j

f

2

GR

Q

(

ord

)

F

o

,

(because

L

(

arity

F

)

is a bijection)

,

L

2

n

f

L

(

arity

F

)

j

f

2

GR

Q

(

ord

)

F

o

.

Theorem 3.97.

GR

Y

(

ord

)

F

=

(

¡[

im

P

¡M

(

arity

F

)

¡

1

j

P

2

Y

i

2

dom

F

F

i

0

)

:

Proof.

From the lemma, because

L

(

arity

F

)

is a bijection.

Theorem 3.98.

GR

Y

(

ord

)

F

=

(

[

i

2

dom

F

¡

P

i

¡M

(

arity

F

)

¡

1

j

P

2

Y

i

2

dom

F

F

i

0

)

:

Proof.

From the previous theorem.

Theorem 3.99.

GR

Y

(

ord

)

F

=

(

[

im

P

j

P

2

Y

i

2

dom

F

f

¡M

(

arity

F

)

¡

1

j

f

2

F

i

0

)

:

3.8 Infinite associativity and ordinated product

47