 3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

43

3.8.4.5.

Definition

with

composition

for

every

multiplier.

q

(

F

)

i

def

=

(curry(

L

(arity

F

)))

i

.

Proposition

246

.

Q

(ord)

F

=

L

f

P

(arity

F

)

i

dom

F

:

L

q

(

F

)

i

GR

F

i

.

Proof.

GR

Q

(ord)

F

=

concat

z

z

Q

(GR

F

)

;

GR

Q

(ord)

F

=

uncurry(

z

)

(

L

(arity

f

)

)

1

z

Q

i

dom

F

f

arity

Fi

,

i

dom

F

:

z

(

i

)

GR

F

i

.

Let

L

= uncurry(

z

). Then

z

= curry(

L

).

GR

Q

(ord)

F

=

L

(

L

(arity

f

)

)

1

curry(

L

)

Q

i

dom

F

f

arity

Fi

,

i

dom

F

:curry(

L

)

i

GR

F

i

;

GR

Q

(ord)

F

=

(

L

(

L

(arity

f

)

)

1

L

f

`

i

dom

F

arity

Fi

,

i

dom

F

:curry(

L

)

i

GR

F

i

)

;

GR

Q

(ord)

F

=

L

f

P

(arity

f

)

i

dom

F

:curry

(

L

L

(arity

F

)

)

i

GR

F

i

;

(curry(

L

L

(arity

F

))

i

)

x

=

L

((curry(

L

(arity

F

))

i

)

x

) =

L

(

q

(

F

)

i

x

) = (

L

q

(

F

)

i

)

x

;

curry(

L

L

(arity

F

))

i

=

L

q

(

F

)

i

;

Q

(ord)

F

=

L

f

P

(arity

F

)

i

dom

F

:

L

q

(

F

)

i

GR

F

i

.

Corollary

247

.

Q

(ord)

F

=

(

L

(

S

im(GR

F

)

)

P

(arity

F

)

i

dom

F

:

L

q

(

F

)

i

GR

F

i

)

.

Corollary

248

.

Q

(ord)

F

is small if

F

is small.

3.8.4.6.

Definition with shifting arguments.

Let

F

0

i

=

n

L

Pr

1

|

{

i

arity

Fi

L

GR

F

i

o

.

Proposition

249

.

F

0

i

=

n

L

Pr

1

|

{

i

f

L

GR

F

i

o

.

Proof.

If

L

GR

F

i

then dom

L

= arity

F

i

. Thus

L

Pr

1

|

{

i

arity

F

i

=

L

Pr

1

|

{

i

dom

L

=

L

Pr

1

|

{

i

f

.

Proposition

250

.

F

0

i

is an (

{

i

} ×

arity

F

i

)-ary relation.

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

251

.

`

(arity

F

) =

S

i

dom

F

(

{

i

} ×

arity

F

i

) =

S

i

dom

F

dom

F

0

i

.

Lemma

252

.

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

.