let A, B, C be Ordinal; :: thesis: ( A c= B implies C *^ A c= C *^ B )
assume A1: A c= B ; :: thesis: C *^ A c= C *^ B

now :: thesis: ( B <> 0 implies C *^ A c= C *^ B )

defpred S₁[ Ordinal] means $1 *^ A c= $1 *^ B;
assume A2: B <> 0 ; :: thesis: C *^ A c= C *^ B
A3: for C being Ordinal st ( for D being Ordinal st D in C holds
S₁[D] ) holds
S₁[C]

proof

let C be Ordinal; :: thesis: ( ( for D being Ordinal st D in C holds
S₁[D] ) implies S₁[C] )
assume A4: for D being Ordinal st D in C holds
D *^ A c= D *^ B ; :: thesis: S₁[C]

A5: now :: thesis: ( ex D being Ordinal st C = succ D implies S₁[C] )

given D being Ordinal such that A6: C = succ D ; :: thesis: S₁[C]
D *^ A c= D *^ B by A4, A6, ORDINAL1:6;
then A7: (D *^ A) +^ A c= (D *^ B) +^ A by Th34;
A8: ( C *^ A = (D *^ A) +^ A & C *^ B = (D *^ B) +^ B ) by A6, Th36;
(D *^ B) +^ A c= (D *^ B) +^ B by A1, Th33;
hence S₁[C] by A7, A8, XBOOLE_1:1; :: thesis: verum

end;

A9: now :: thesis: ( C <> 0 & ( for D being Ordinal holds C <> succ D ) implies S₁[C] )

deffunc H₁( Ordinal) -> Ordinal = $1 *^ A;
assume that
A10: C <> 0 and
A11: for D being Ordinal holds C <> succ D ; :: thesis: S₁[C]
consider fi being Ordinal-Sequence such that
A12: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();

now :: thesis: for D being Ordinal st D in rng fi holds
D in C *^ B

let D be Ordinal; :: thesis: ( D in rng fi implies D in C *^ B )
assume D in rng fi ; :: thesis: D in C *^ B
then consider x being object such that
A13: x in dom fi and
A14: D = fi . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A13;
A15: x *^ B in C *^ B by A2, A12, A13, Th40;
( D = x *^ A & x *^ A c= x *^ B ) by A4, A12, A13, A14;
hence D in C *^ B by A15, ORDINAL1:12; :: thesis: verum

end;

then A16: sup (rng fi) c= C *^ B by Th20;
C is limit_ordinal by A11, ORDINAL1:29;
then A17: C *^ A = union (sup fi) by A10, A12, Th37
.= union (sup (rng fi)) ;
union (sup (rng fi)) c= sup (rng fi) by Th5;
hence S₁[C] by A17, A16, XBOOLE_1:1; :: thesis: verum

end;

now :: thesis: ( C = 0 implies S₁[C] )

assume C = 0 ; :: thesis: S₁[C]
then C *^ A = 0 by Th35;
hence S₁[C] ; :: thesis: verum

end;

hence S₁[C] by A5, A9; :: thesis: verum

end;

for C being Ordinal holds S₁[C] from ORDINAL1:sch 2(A3);
hence C *^ A c= C *^ B ; :: thesis: verum

end;

hence C *^ A c= C *^ B by A1; :: thesis: verum