let W be Universe; :: thesis: for a being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let a be Ordinal of W; :: thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let phi be Ordinal-Sequence of W; :: thesis: ( omega in W & phi is increasing & phi is continuous implies ex b being Ordinal of W st
( a in b & phi . b = b ) )
assume A1: ( omega in W & phi is increasing & phi is continuous ) ; :: thesis: ex b being Ordinal of W st
( a in b & phi . b = b )
deffunc H₁( Ordinal of W) -> Element of W = (succ a) +^ (phi . $1);
consider xi being Ordinal-Sequence of W such that
A2: for b being Ordinal of W holds xi . b = H₁(b) from ORDINAL4:sch 2();
A3: ( dom phi = On W & dom xi = On W ) by FUNCT_2:def 1;
for A being Ordinal st A in dom phi holds
xi . A = (succ a) +^ (phi . A)

proof

let A be Ordinal; :: thesis: ( A in dom phi implies xi . A = (succ a) +^ (phi . A) )
assume A in dom phi ; :: thesis: xi . A = (succ a) +^ (phi . A)
then reconsider b = A as Ordinal of W by A3, ZF_REFLE:8;
( xi . b = (succ a) +^ (phi . b) & phi . b = phi . b ) by A2;
hence xi . A = (succ a) +^ (phi . A) ; :: thesis: verum

end;

then xi = (succ a) +^ phi by A3, ORDINAL3:def 2;
then ( xi is increasing & xi is continuous ) by A1, Th15, Th17;
then consider A being Ordinal such that
A4: ( A in dom xi & xi . A = A ) by A1, ORDINAL4:38;
reconsider b = A as Ordinal of W by A3, A4, ZF_REFLE:8;
take b ; :: thesis: ( a in b & phi . b = b )
( succ a c= (succ a) +^ (phi . b) & a in succ a & b = (succ a) +^ (phi . b) & b c= phi . b & phi . b c= (succ a) +^ (phi . b) ) by A1, A2, A3, A4, ORDINAL1:10, ORDINAL3:27, ORDINAL4:10;
hence ( a in b & phi . b = b ) by XBOOLE_0:def 10; :: thesis: verum