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

defpred S₁[ Ordinal] means $1 *^ A c= $1 *^ B;
assume A2: B <> {} ; :: 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

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 Th51;
A8: ( C *^ A = (D *^ A) +^ A & C *^ B = (D *^ B) +^ B ) by A6, Th53;
(D *^ B) +^ A c= (D *^ B) +^ B by A1, Th50;
hence S₁[C] by A7, A8, XBOOLE_1:1; :: thesis: verum

end;

A9: now

deffunc H₁( Ordinal) -> Ordinal = $1 *^ A;
assume that
A10: C <> {} 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

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 set 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, Th57;
( 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 Th28;
C is limit_ordinal by A11, ORDINAL1:29;
then A17: C *^ A = union (sup fi) by A10, A12, Th54
.= 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

assume C = {} ; :: thesis: S₁[C]
then C *^ A = {} by Th52;
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