3.7. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

53

Proof.

Let

L

0

L

f

`

i

dom

F

arity

Fi

curry(

L

)

Q

(GR

F

)

. Then

L

0

f

`

i

dom

F

arity

F

i

and

curry(

L

0

)

Q

(GR

F

).

Let

P

=

λi

dom

F

:

L

0

|

{

i

arity

F

i

. Then

P

`

i

dom

F

f

{

i

arity

F

i

and

S

im

P

=

L

0

. So

L

0

S

im

P

P

`

i

dom

F

f

{

i

arity

Fi

curry(

S

im

P

)

Q

(GR

F

)

.

Let now

L

0

S

im

P

P

`

i

dom

F

f

{

i

arity

Fi

curry(

S

im

P

)

Q

(GR

F

)

. Then there ex-

ists

P

`

i

dom

F

f

{

i

arity

F

i

such that

L

0

=

S

im

P

and curry(

L

0

)

Q

(GR

F

).

Evidently

L

0

f

`

i

dom

F

arity

F

i

. So

L

0

L

f

`

i

dom

F

arity

Fi

curry(

L

)

Q

(GR

F

)

.

Lemma

307

.

f

L

(arity

F

)

f

GR

Q

(ord)

F

=

S

im

P

P

Q

i

dom

F

F

0

i

.

Proof.

L

S

im

P

P

Q

i

dom

F

F

0

i

L

S

im

P

P

`

i

dom

F

f

{

i

arity

F

i

curry(

S

im

P

)

Q

(GR

F

)

L

f

`

i

dom

F

arity

F

i

curry(

L

)

Y

(GR

F

)

L

f

`

i

dom

F

arity

F

i

curry(

L

)

(

curry(

f

)

L

(arity

F

)

f

GR

Q

(ord)

F

)

(because

M

(arity

F

) is a bijection)

curry(

L

)

M

(arity

F

)

1

(

curry(

f

)

f

GR

Q

(ord)

F

)

L

M

(arity

F

)

1

(

f

f

GR

Q

(ord)

F

)

(because

M

(arity

F

) is a bijection)

L

(

f

L

(arity

F

)

f

GR

Q

(ord)

F

)

.

Theorem

308

.

GR

Q

(ord)

F

=

(

S

im

P

)

(

L

(arity

F

)

)

1

P

Q

i

dom

F

F

0

i

.

Proof.

From the lemma, because

L

(arity

F

) is a bijection.

Theorem

309

.

GR

Q

(ord)

F

=

S

i

dom

F

P

i

(

L

(arity

f

)

)

1

P

Q

i

dom

F

F

0

i

.

Proof.

From the previous theorem.

Theorem

310

.

GR

Q

(ord)

F

=

S

im

P

P

Q

i

dom

F

f

(

L

(arity

f

)

)

1

f

F

0

i

.

Proof.

From the previous.