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

A1: now :: thesis: ( A <> {} & A is limit_ordinal & A is limit_ordinal implies A *^ B is limit_ordinal )

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:37
.= 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:21;
consider x being object such that
A11: x in dom fi and
A12: D = fi . x by A9, FUNCT_1:def 3;
succ C c= D by A7, A10, ORDINAL1:21;
then A13: succ C in succ D by ORDINAL1:22;
reconsider x = x as Ordinal by A11;
A14: succ x in dom fi by A3, A4, A11, ORDINAL1:28;
then fi . (succ x) = (succ x) *^ B by A4
.= (x *^ B) +^ B by ORDINAL2:36 ;
then (x *^ B) +^ B in rng fi by A14, FUNCT_1:def 3;
then A15: (x *^ B) +^ B in sup (rng fi) by ORDINAL2:19;
A16: (x *^ B) +^ (succ {}) = succ ((x *^ B) +^ {}) by ORDINAL2:28;
B <> {} by A6, ORDINAL2:38;
then {} in B by Th8;
then A17: succ {} c= B by ORDINAL1:21;
A18: (x *^ B) +^ {} = x *^ B by ORDINAL2:27;
x *^ B = fi . x by A4, A11;
then succ D in sup (rng fi) by A12, A17, A16, A18, A15, ORDINAL1:12, ORDINAL2:33;
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:28; :: thesis: verum

end;

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