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

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

assume C = {} ; :: thesis: S₁[C]
then ( C *^ A = {} & C *^ B = {} ) by Th52;
hence S₁[C] ; :: thesis: verum

end;

A6: now

given D being Ordinal such that A7: C = succ D ; :: thesis: S₁[C]
D *^ A c= D *^ B by A4, A7, ORDINAL1:10;
then ( (D *^ A) +^ A c= (D *^ B) +^ A & (D *^ B) +^ A c= (D *^ B) +^ B & C *^ A = (D *^ A) +^ A & C *^ B = (D *^ B) +^ B ) by A1, A7, Th50, Th51, Th53;
hence S₁[C] by XBOOLE_1:1; :: thesis: verum

end;

now

assume A8: ( C <> {} & ( for D being Ordinal holds C <> succ D ) ) ; :: thesis: S₁[C]
then A9: C is limit_ordinal by ORDINAL1:42;
deffunc H₁( Ordinal) -> Ordinal = $1 *^ A;
consider fi being Ordinal-Sequence such that
A10: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A11: C *^ A = union (sup fi) by A8, A9, A10, Th54
.= union (sup (rng fi)) ;

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
A12: ( x in dom fi & D = fi . x ) by FUNCT_1:def 5;
reconsider x = x as Ordinal by A12;
A13: D = x *^ A by A10, A12;
( x *^ A c= x *^ B & x *^ B in C *^ B ) by A2, A4, A10, A12, Th57;
hence D in C *^ B by A13, ORDINAL1:22; :: thesis: verum

end;

then ( sup (rng fi) c= C *^ B & union (sup (rng fi)) c= sup (rng fi) ) by Th5, Th28;
hence S₁[C] by A11, XBOOLE_1:1; :: thesis: verum

end;

hence S₁[C] by A5, A6; :: 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