let A, B, C be Ordinal; :: thesis: ( A in B implies C +^ A in C +^ B )
defpred S₁[ Ordinal] means ( A in $1 implies C +^ A in C +^ $1 );
A1: for B being Ordinal st ( for D being Ordinal st D in B holds
S₁[D] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( ( for D being Ordinal st D in B holds
S₁[D] ) implies S₁[B] )
assume that
A2: for D being Ordinal st D in B & A in D holds
C +^ A in C +^ D and
A3: A in B ; :: thesis: C +^ A in C +^ B

A4: now :: thesis: ( ex D being Ordinal st B = succ D implies C +^ A in C +^ B )

given D being Ordinal such that A5: B = succ D ; :: thesis: C +^ A in C +^ B

A6: now :: thesis: ( A in D implies C +^ A in C +^ B )

assume A in D ; :: thesis: C +^ A in C +^ B
then A7: C +^ A in C +^ D by A2, A5, ORDINAL1:6;
( succ (C +^ D) = C +^ (succ D) & C +^ D in succ (C +^ D) ) by Th28, ORDINAL1:6;
hence C +^ A in C +^ B by A5, A7, ORDINAL1:10; :: thesis: verum

end;

now :: thesis: ( not A in D implies C +^ A in C +^ B )

assume A8: not A in D ; :: thesis: C +^ A in C +^ B
( A c< D iff ( A c= D & A <> D ) ) ;
then C +^ A in succ (C +^ D) by A3, A5, A8, ORDINAL1:11, ORDINAL1:22;
hence C +^ A in C +^ B by A5, Th28; :: thesis: verum

end;

hence C +^ A in C +^ B by A6; :: thesis: verum

end;

now :: thesis: ( ( for D being Ordinal holds B <> succ D ) implies C +^ A in C +^ B )

deffunc H₁( Ordinal) -> Ordinal = C +^ $1;
consider fi being Ordinal-Sequence such that
A9: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
fi . A = C +^ A by A3, A9;
then A10: C +^ A in rng fi by A3, A9, FUNCT_1:def 3;
assume for D being Ordinal holds B <> succ D ; :: thesis: C +^ A in C +^ B
then B is limit_ordinal by ORDINAL1:29;
then C +^ B = sup fi by A3, A9, Th29
.= sup (rng fi) ;
hence C +^ A in C +^ B by A10, Th19; :: thesis: verum

end;

hence C +^ A in C +^ B by A4; :: thesis: verum

end;

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