3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

45

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 exists

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

S

im

P

P

`

i

dom

F

f

{

i

arity

Fi

curry(

S

im

P

)

Q

(GR

F

)

.

Lemma

255

.

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

256

.

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

257

.

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

258

.

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.

Remark

259

.

Note that the above formulas contain both

S

i

dom

F

dom

F

0

i

and

S

i

dom

F

F

0

i

. These forms are similar but different.