3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

44

Proof.

For every

P

`

i

dom

F

f

{

i

arity

F

i

we have:

P

Y

i

=dom

F

F

0

i

P

z

f

dom

F

i

dom

F

:

z

(

i

)

F

0

i

P

f

dom

F

∧ ∀

i

dom

F

:

P

(

i

)

F

0

i

P

f

dom

F

∧ ∀

i

dom

F

L

GR

F

i

:

P

i

=

L

(Pr

1

|

{

i

f

)

P

f

dom

F

∧ ∀

i

dom

F

L

GR

F

i

: (

P

i

f

{

i

arity

F

i

∧ ∀

x

arity

F

i

:

P

i

(

i

;

x

) =

Lx

)

P

f

dom

F

∧ ∀

i

dom

F

L

GR

F

i

: (

P

i

f

{

i

arity

F

i

curry(

P

i

)

i

=

L

)

P

f

dom

F

∧ ∀

i

dom

F

L

GR

F

i

: (

P

i

f

{

i

arity

F

i

curry(

P

i

)

i

=

L

)

P

f

dom

F

∧ ∀

i

dom

F

: (

P

i

f

{

i

arity

F

i

curry(

P

i

)

i

GR

F

i

)

i

dom

F

Q

i

(

f

arity

F

i

)

{

i

}

: (

P

i

= uncurry(

Q

i

)

(

Q

i

)

i

f

arity

F

i

Q

i

i

GR

F

i

)

i

dom

F

Q

i

(

f

arity

F

i

)

{

i

}

:

P

i

= uncurry(

Q

i

)

[

i

dom

F

Q

i

!

i

GR

F

i

!

i

dom

F

Q

i

(

f

arity

F

i

)

{

i

}

:

P

i

= uncurry(

Q

i

)

[

i

dom

F

Q

i

Y

(GR

F

)

!

i

dom

F

:

[

i

dom

F

curry(

P

i

)

Y

(GR

F

)

curry

[

i

dom

F

P

i

Y

(GR

F

)

!

Y

(GR

F

)

curry

[

im

P

Y

(GR

F

)

.

Lemma

253

.

curry(

f

)

L

(arity

F

)

f

GR

Q

(ord)

F

=

Q

(GR

F

).

Proof.

First GR

Q

(ord)

F

=

uncurry(

z

)

(

L

(dom

z

)

)

1

z

Q

(GR

F

)

, that is

f

f

GR

Q

(ord)

F

=

uncurry(

z

)

(

L

(arity

F

)

)

1

z

Q

(GR

F

)

.

Since

L

(arity

F

) is a bijection, we have

f

L

(arity

F

)

f

GR

Q

(ord)

F

=

uncurry(

z

)

z

Q

(GR

F

)

what is equivalent to

curry(

f

)

L

(arity

F

)

f

GR

Q

(ord)

F

=

z

z

Q

(GR

F

)

that is

curry(

f

)

L

(arity

F

)

f

GR

Q

(ord)

F

=

Q

(GR

F

).

Lemma

254

.

S

im

P

P

`

i

dom

F

f

{

i

arity

Fi

curry(

S

im

P

)

Q

(GR

F

)

=

L

f

`

i

dom

F

arity

Fi

curry(

L

)

Q

(GR

F

)

.

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

).