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 H1( 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 = H1(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;
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