background image

Thus uncurry

(

uncurry

S

)(

i

; (

x

;

y

)) = (

uncurry

(

uncurry

S

))((

i

;

x

);

y

)

and thus evidently

uncurry

(

uncurry

S

)

uncurry

(

uncurry

S

)

.

Theorem 3.106.

concat is an innitely associative function.

Proof.

concat

(

J

x

K

) =

x

for a function

x

taking an ordinal number of argument is obvious. It is

remained to prove

concat

(

concat

S

) =

concat

(

concat

S

);

We have, using the lemmas, concat

(

concat

S

)

uncurry

(

concat

S

)

(by lemma

3.104

)

uncurry

(

uncurry

S

)

uncurry

(

uncurry

S

)

uncurry

(

concat

S

)

concat

(

concat

S

)

.

Corollary 3.107.

Ordinated product is an innitely associative function.

3.8 Infinite associativity and ordinated product

49