let A, B, C be Ordinal; :: thesis: ( A c= B implies A +^ C c= B +^ C )
defpred S₁[ Ordinal] means A +^ $1 c= B +^ $1;
assume A1: A c= B ; :: thesis: A +^ C c= B +^ C
A2: 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 A3: for D being Ordinal st D in C holds
A +^ D c= B +^ D ; :: thesis: S₁[C]

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

given D being Ordinal such that A5: C = succ D ; :: thesis: S₁[C]
A6: B +^ C = succ (B +^ D) by A5, Th28;
( A +^ D c= B +^ D & A +^ C = succ (A +^ D) ) by A3, A5, Th28, ORDINAL1:6;
hence S₁[C] by A6, Th1; :: thesis: verum

end;

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

deffunc H₁( Ordinal) -> Ordinal = A +^ $1;
assume that
A8: C <> 0 and
A9: for D being Ordinal holds C <> succ D ; :: thesis: S₁[C]
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: now :: thesis: for D being Ordinal st D in rng fi holds
D in B +^ C

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

end;

C is limit_ordinal by A9, ORDINAL1:29;
then A +^ C = sup fi by A8, A10, Th29
.= sup (rng fi) ;
hence S₁[C] by A11, Th20; :: thesis: verum

end;

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

assume A15: C = 0 ; :: thesis: S₁[C]
then A +^ C = A by Th27;
hence S₁[C] by A1, A15, Th27; :: thesis: verum

end;

hence S₁[C] by A4, A7; :: thesis: verum

end;

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