let A, B be Ordinal; :: thesis: ( A is limit_ordinal implies A *^ B is limit_ordinal )
assume A1: A is limit_ordinal ; :: thesis: A *^ B is limit_ordinal

now

assume A2: ( A <> {} & A is limit_ordinal ) ; :: thesis: A *^ B is limit_ordinal
deffunc H₁( Ordinal) -> set = $1 *^ B;
consider fi being Ordinal-Sequence such that
A3: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = H₁(C) ) ) from ORDINAL2:sch 3();
A4: A *^ B = union (sup fi) by A2, A3, ORDINAL2:54
.= union (sup (rng fi)) ;
for C being Ordinal st C in A *^ B holds
succ C in A *^ B

proof

let C be Ordinal; :: thesis: ( C in A *^ B implies succ C in A *^ B )
assume A5: C in A *^ B ; :: thesis: succ C in A *^ B
then consider X being set such that
A6: ( C in X & X in sup (rng fi) ) by A4, TARSKI:def 4;
reconsider X = X as Ordinal by A6;
consider D being Ordinal such that
A7: ( D in rng fi & X c= D ) by A6, ORDINAL2:29;
consider x being set such that
A8: ( x in dom fi & D = fi . x ) by A7, FUNCT_1:def 5;
reconsider x = x as Ordinal by A8;
B <> {} by A5, ORDINAL2:55;
then {} in B by Th10;
then ( succ {} c= B & (x *^ B) +^ (succ {} ) = succ ((x *^ B) +^ {} ) & (x *^ B) +^ {} = x *^ B ) by ORDINAL1:33, ORDINAL2:44, ORDINAL2:45;
then A9: ( succ (x *^ B) c= (x *^ B) +^ B & x *^ B = fi . x ) by A3, A8, ORDINAL2:50;
A10: succ x in dom fi by A2, A3, A8, ORDINAL1:41;
then fi . (succ x) = (succ x) *^ B by A3
.= (x *^ B) +^ B by ORDINAL2:53 ;
then ( (x *^ B) +^ B in rng fi & C in D ) by A6, A7, A10, FUNCT_1:def 5;
then ( (x *^ B) +^ B in sup (rng fi) & succ C c= D ) by ORDINAL1:33, ORDINAL2:27;
then ( succ C in succ D & succ D in sup (rng fi) ) by A8, A9, ORDINAL1:22, ORDINAL1:34;
hence succ C in A *^ B by A4, TARSKI:def 4; :: thesis: verum

end;

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

end;

hence A *^ B is limit_ordinal by A1, ORDINAL2:52; :: thesis: verum