let A, B, C be Ordinal; :: thesis: (A *^ B) *^ C = A *^ (B *^ C)
defpred S₁[ Ordinal] means ($1 *^ B) *^ C = $1 *^ (B *^ C);
( {} *^ B = {} & {} *^ C = {} & {} *^ (B *^ C) = {} ) by ORDINAL2:52;
then A1: S₁[ {} ] ;
A2: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A3: (A *^ B) *^ C = A *^ (B *^ C) ; :: thesis: S₁[ succ A]
thus ((succ A) *^ B) *^ C = ((A *^ B) +^ B) *^ C by ORDINAL2:53
.= (A *^ (B *^ C)) +^ (B *^ C) by A3, Th54
.= (A *^ (B *^ C)) +^ (1 *^ (B *^ C)) by ORDINAL2:56
.= (A +^ 1) *^ (B *^ C) by Th54
.= (succ A) *^ (B *^ C) by ORDINAL2:48 ; :: thesis: verum

end;

A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for D being Ordinal st D in A holds
S₁[D] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for D being Ordinal st D in A holds
S₁[D] ) implies S₁[A] )
assume that
A5: ( A <> {} & A is limit_ordinal ) and
A6: for D being Ordinal st D in A holds
(D *^ B) *^ C = D *^ (B *^ C) ; :: thesis: S₁[A]

A7: now

assume ( not 1 in B or not 1 in C ) ; :: thesis: S₁[A]
then A8: ( B = {} or B = 1 or C = {} or C = 1 ) by Th19, ORDINAL1:26;
( A *^ {} = {} & {} *^ C = {} & A *^ 1 = A & 1 *^ C = C & (A *^ B) *^ {} = {} & B *^ {} = {} & (A *^ B) *^ 1 = A *^ B & B *^ 1 = B ) by ORDINAL2:52, ORDINAL2:55, ORDINAL2:56;
hence S₁[A] by A8; :: thesis: verum

end;

now

assume A9: ( 1 in B & 1 in C ) ; :: thesis: S₁[A]
1 = 1 *^ 1 by ORDINAL2:56;
then A10: ( 1 in B *^ C & C <> {} ) by A9, Th22;
deffunc H₁( Ordinal) -> set = $1 *^ B;
consider fi being Ordinal-Sequence such that
A11: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
( dom (fi *^ C) = A & ( for D being Ordinal st D in A holds
(fi *^ C) . D = D *^ (B *^ C) ) )

proof

thus dom (fi *^ C) = A by A11, Def5; :: thesis: for D being Ordinal st D in A holds
(fi *^ C) . D = D *^ (B *^ C)
let D be Ordinal; :: thesis: ( D in A implies (fi *^ C) . D = D *^ (B *^ C) )
assume D in A ; :: thesis: (fi *^ C) . D = D *^ (B *^ C)
then ( (fi *^ C) . D = (fi . D) *^ C & fi . D = D *^ B & (D *^ B) *^ C = D *^ (B *^ C) ) by A6, A11, Def5;
hence (fi *^ C) . D = D *^ (B *^ C) ; :: thesis: verum

end;

then ( A *^ B = sup fi & A *^ (B *^ C) = sup (fi *^ C) & A *^ B is limit_ordinal ) by A5, A9, A10, A11, Th48, Th57;
hence S₁[A] by A5, A9, A11, Th52; :: thesis: verum

end;

hence S₁[A] by A7; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A1, A2, A4);
hence (A *^ B) *^ C = A *^ (B *^ C) ; :: thesis: verum