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

A1: now

deffunc H₁( Ordinal) -> set = $1 *^ B;
assume that
A2: A <> {} and
A3: A is limit_ordinal ; :: thesis: ( A is limit_ordinal implies A *^ B is limit_ordinal )
consider fi being Ordinal-Sequence such that
A4: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = H₁(C) ) ) from ORDINAL2:sch 3();
A5: A *^ B = union (sup fi) by A2, A3, A4, 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 A6: C in A *^ B ; :: thesis: succ C in A *^ B
then consider X being set such that
A7: C in X and
A8: X in sup (rng fi) by A5, TARSKI:def 4;
reconsider X = X as Ordinal by A8;
consider D being Ordinal such that
A9: D in rng fi and
A10: X c= D by A8, ORDINAL2:29;
consider x being set such that
A11: x in dom fi and
A12: D = fi . x by A9, FUNCT_1:def 5;
succ C c= D by A7, A10, ORDINAL1:33;
then A13: succ C in succ D by ORDINAL1:34;
reconsider x = x as Ordinal by A11;
A14: succ x in dom fi by A3, A4, A11, ORDINAL1:41;
then fi . (succ x) = (succ x) *^ B by A4
.= (x *^ B) +^ B by ORDINAL2:53 ;
then (x *^ B) +^ B in rng fi by A14, FUNCT_1:def 5;
then A15: (x *^ B) +^ B in sup (rng fi) by ORDINAL2:27;
A16: (x *^ B) +^ (succ {} ) = succ ((x *^ B) +^ {} ) by ORDINAL2:45;
B <> {} by A6, ORDINAL2:55;
then {} in B by Th10;
then A17: succ {} c= B by ORDINAL1:33;
A18: (x *^ B) +^ {} = x *^ B by ORDINAL2:44;
x *^ B = fi . x by A4, A11;
then succ D in sup (rng fi) by A12, A17, A16, A18, A15, ORDINAL1:22, ORDINAL2:50;
hence succ C in A *^ B by A5, A13, TARSKI:def 4; :: thesis: verum

end;

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

end;

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