let A, B be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies B +^ A is limit_ordinal )
assume A1: ( A <> {} & A is limit_ordinal ) ; :: thesis: B +^ A is limit_ordinal
{} c= A by XBOOLE_1:2;
then {} c< A by A1, XBOOLE_0:def 8;
then A2: {} in A by ORDINAL1:21;
deffunc H₁( Ordinal) -> set = B +^ $1;
consider L being Ordinal-Sequence such that
A3: ( dom L = A & ( for C being Ordinal st C in A holds
L . C = H₁(C) ) ) from ORDINAL2:sch 3();
A4: B +^ A = sup L by A1, A3, ORDINAL2:46
.= 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 A5: C in B +^ A ; :: thesis: succ C in B +^ A

A6: now

assume C in B ; :: thesis: succ C in B +^ A
then succ C c= B by ORDINAL1:33;
then ( (succ C) +^ {} = succ C & (succ C) +^ {} c= B +^ {} & B +^ {} in B +^ A ) by A2, ORDINAL2:44, ORDINAL2:49, ORDINAL2:51;
hence succ C in B +^ A by ORDINAL1:22; :: thesis: verum

end;

now

assume not C in B ; :: thesis: succ C in B +^ A
then B c= C by ORDINAL1:26;
then consider D being Ordinal such that
A7: C = B +^ D by Th30;

now

assume not D in A ; :: thesis: contradiction
then B +^ A c= B +^ D by ORDINAL1:26, ORDINAL2:50;
then C in C by A5, A7;
hence contradiction ; :: thesis: verum

end;

then A8: ( succ D in A & L . D = B +^ D ) by A1, A3, ORDINAL1:41;
then L . (succ D) = B +^ (succ D) by A3
.= succ (B +^ D) by ORDINAL2:45 ;
then succ C in rng L by A3, A7, A8, FUNCT_1:def 5;
hence succ C in B +^ A by A4, ORDINAL2:27; :: thesis: verum

end;

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

end;

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