background image

3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

47

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,

FiXme

: Say that

implies equality.

concat(concat

S

)

uncurry(concat

S

)

(by lemma

263

)

uncurry(uncurry

S

)

uncurry(uncurry

S

)

uncurry(concat

S

)

concat(concat

S

)

.

Corollary

266

.

Ordinated product is an infinitely associative function.