background image

3.7. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

52

Proof.

We need to prove that dom

L

Pr

1

|

{

i

arity

F

i

=

{

i

} ×

arity

F

i

for

L

GR

F

i

, but that’s obvious.

Obvious

306

.

`

(arity

F

) =

S

i

dom

F

(

{

i

} ×

arity

F

i

) =

S

i

dom

F

dom

F

0

i

.

Lemma

307

.

P

Q

i

dom

F

F

0

i

curry(

S

im

P

)

Q

(GR

F

) for a (dom

F

)-

indexed family

P

where

P

i

f

{

i

arity

F

i

for every

i

dom

F

, that is for

P

`

i

dom

F

f

{

i

arity

F

i

.

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

: (

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

)

curry

[

im

P

Y

(GR

F

)

.

Lemma

308

.

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

309

.

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

)

.