let A, B, C be Ordinal; :: thesis: ( A in B *^ C & B is limit_ordinal implies ex D being Ordinal st
( D in B & A in D *^ C ) )
assume A1: ( A in B *^ C & B is limit_ordinal ) ; :: thesis: ex D being Ordinal st
( D in B & A in D *^ C )
then A2: ( B <> {} & C <> {} ) by ORDINAL2:52, ORDINAL2:55;
deffunc H₁( Ordinal) -> set = $1 *^ C;
consider fi being Ordinal-Sequence such that
A3: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
B *^ C = union (sup fi) by A1, A2, A3, ORDINAL2:54
.= union (sup (rng fi)) ;
then consider X being set such that
A4: ( A in X & X in sup (rng fi) ) by A1, TARSKI:def 4;
reconsider X = X as Ordinal by A4;
consider D being Ordinal such that
A5: ( D in rng fi & X c= D ) by A4, ORDINAL2:29;
consider x being set such that
A6: ( x in dom fi & D = fi . x ) by A5, FUNCT_1:def 5;
reconsider x = x as Ordinal by A6;
take E = succ x; :: thesis: ( E in B & A in E *^ C )
thus E in B by A1, A3, A6, ORDINAL1:41; :: thesis: A in E *^ C
A7: E *^ C = (x *^ C) +^ C by ORDINAL2:53
.= D +^ C by A3, A6 ;
( D +^ {} = D & {} in C ) by A2, Th10, ORDINAL2:44;
then ( D in E *^ C & A in D ) by A4, A5, A7, ORDINAL2:49;
hence A in E *^ C by ORDINAL1:19; :: thesis: verum