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

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

A7: now

A8: ( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def 8;
assume not A in D ; :: thesis: C +^ A in C +^ B
then ( C +^ A in succ (C +^ D) & succ (C +^ D) = C +^ (succ D) ) by A3, A5, A8, Th45, ORDINAL1:21, ORDINAL1:34;
hence C +^ A in C +^ B by A5; :: thesis: verum

end;

now

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

end;

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

end;

now

assume for D being Ordinal holds B <> succ D ; :: thesis: C +^ A in C +^ B
then A9: B is limit_ordinal by ORDINAL1:42;
deffunc H₁( Ordinal) -> Ordinal = C +^ $1;
consider fi being Ordinal-Sequence such that
A10: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A11: C +^ B = sup fi by A3, A9, A10, Th46
.= sup (rng fi) ;
fi . A = C +^ A by A3, A10;
then C +^ A in rng fi by A3, A10, FUNCT_1:def 5;
hence C +^ A in C +^ B by A11, Th27; :: 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