let A, B, C be Ordinal; (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]
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;
( 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)
;
S1[A]
A8:
now ( 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
;
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) ) )
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;
verum end;
now ( ( not 1 in B or not 1 in C ) implies S1[A] )end;
hence
S1[
A]
by A8;
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)
; verum