let A, B, C be Ordinal; :: thesis: (A *^ B) *^ C = A *^ (B *^ C)
defpred S1[ Ordinal] means ($1 *^ B) *^ C = $1 *^ (B *^ C);
A1: {} *^ C = {} by ORDINAL2:35;
A2: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; :: thesis: ( S1[A] implies S1[ succ A] )
assume A3: (A *^ B) *^ C = A *^ (B *^ C) ; :: thesis: S1[ succ A]
thus ((succ A) *^ B) *^ C = ((A *^ B) +^ B) *^ C by ORDINAL2:36
.= (A *^ (B *^ C)) +^ (B *^ C) by A3, Th46
.= (A *^ (B *^ C)) +^ (1 *^ (B *^ C)) by ORDINAL2:39
.= (A +^ 1) *^ (B *^ C) by Th46
.= (succ A) *^ (B *^ C) by ORDINAL2:31 ; :: thesis: verum
end;
A4: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for D being Ordinal st D in A holds
S1[D] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for D being Ordinal st D in A holds
S1[D] ) implies S1[A] )
assume that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: for D being Ordinal st D in A holds
(D *^ B) *^ C = D *^ (B *^ C) ; :: thesis: S1[A]
A8: now :: thesis: ( 1 in B & 1 in C implies S1[A] )
deffunc H1( Ordinal) -> set = $1 *^ B;
assume that
A9: 1 in B and
A10: 1 in C ; :: thesis: S1[A]
consider fi being Ordinal-Sequence such that
A11: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H1(D) ) ) from ORDINAL2:sch 3();
A12: ( 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, Def4; :: 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 A13: D in A ; :: thesis: (fi *^ C) . D = D *^ (B *^ C)
then A14: fi . D = D *^ B by A11;
(fi *^ C) . D = (fi . D) *^ C by A11, A13, Def4;
hence (fi *^ C) . D = D *^ (B *^ C) by A7, A13, A14; :: thesis: verum
end;
1 = 1 *^ 1 by ORDINAL2:39;
then 1 in B *^ C by A9, A10, Th19;
then A15: A *^ (B *^ C) = sup (fi *^ C) by A5, A6, A12, Th49;
A *^ B = sup fi by A5, A6, A9, A11, Th49;
hence S1[A] by A5, A6, A10, A11, A15, Th40, Th44; :: thesis: verum
end;
now :: thesis: ( ( not 1 in B or not 1 in C ) implies S1[A] )
assume ( not 1 in B or not 1 in C ) ; :: thesis: S1[A]
then A16: ( B = {} or B = 1 or C = {} or C = 1 ) by Th16, ORDINAL1:16;
A17: {} *^ C = {} by ORDINAL2:35;
A18: (A *^ B) *^ 1 = A *^ B by ORDINAL2:39;
A19: (A *^ B) *^ {} = {} by ORDINAL2:38;
A20: A *^ 1 = A by ORDINAL2:39;
A *^ {} = {} by ORDINAL2:38;
hence S1[A] by A16, A17, A20, A19, A18, ORDINAL2:38, ORDINAL2:39; :: thesis: verum
end;
hence S1[A] by A8; :: thesis: verum
end;
{} *^ B = {} by ORDINAL2:35;
then A21: S1[ 0 ] by A1, ORDINAL2:35;
for A being Ordinal holds S1[A] from ORDINAL2:sch 1(A21, A2, A4);
 hence (A *^ B) *^ C = A *^ (B *^ C) ; :: thesis: verum