let A, B be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies B +^ A is limit_ordinal )
assume that
A1: A <> {} and
A2: A is limit_ordinal ; :: thesis: B +^ A is limit_ordinal
{} c= A ;
then A3: {} c< A by A1;
deffunc H₁( Ordinal) -> set = B +^ $1;
consider L being Ordinal-Sequence such that
A4: ( dom L = A & ( for C being Ordinal st C in A holds
L . C = H₁(C) ) ) from ORDINAL2:sch 3();
A5: B +^ A = sup L by A1, A2, A4, ORDINAL2:29
.= sup (rng L) ;
for C being Ordinal st C in B +^ A holds
succ C in B +^ A

proof

let C be Ordinal; :: thesis: ( C in B +^ A implies succ C in B +^ A )
assume A6: C in B +^ A ; :: thesis: succ C in B +^ A

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

assume not C in B ; :: thesis: succ C in B +^ A
then consider D being Ordinal such that
A8: C = B +^ D by Th27, ORDINAL1:16;

now :: thesis: D in A

assume not D in A ; :: thesis: contradiction
then B +^ A c= B +^ D by ORDINAL1:16, ORDINAL2:33;
then C in C by A6, A8;
hence contradiction ; :: thesis: verum

end;

then A9: succ D in A by A2, ORDINAL1:28;
then L . (succ D) = B +^ (succ D) by A4
.= succ (B +^ D) by ORDINAL2:28 ;
then succ C in rng L by A4, A8, A9, FUNCT_1:def 3;
hence succ C in B +^ A by A5, ORDINAL2:19; :: thesis: verum

end;

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

assume C in B ; :: thesis: succ C in B +^ A
then A10: succ C c= B by ORDINAL1:21;
A11: (succ C) +^ {} = succ C by ORDINAL2:27;
B +^ {} in B +^ A by A3, ORDINAL1:11, ORDINAL2:32;
hence succ C in B +^ A by A10, A11, ORDINAL1:12, ORDINAL2:34; :: thesis: verum

end;

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

end;

hence B +^ A is limit_ordinal by ORDINAL1:28; :: thesis: verum