let a be ordinal number ; :: thesis: ex b being ordinal number st
( a in b & b is epsilon )
deffunc H₁( Ordinal) -> set = exp omega ,$1;
A1: for a, b being ordinal number st a in b holds
H₁(a) in H₁(b) by ORDINAL4:24;

A2: now

let a be ordinal number ; :: thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi )
assume B1: ( not a is empty & a is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi
let phi be Ordinal-Sequence; :: thesis: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H₁(b) ) implies H₁(a) is_limes_of phi )
assume B2: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H₁(b) ) ) ; :: thesis: H₁(a) is_limes_of phi
phi is non-decreasing

proof

let b be ordinal number ; :: according to ORDINAL5:def 2 :: thesis: for b being ordinal number st b in b & b in dom phi holds
phi . b c= phi . b
let c be ordinal number ; :: thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume B3: ( b in c & c in dom phi ) ; :: thesis: phi . b c= phi . c
then ( phi . b = H₁(b) & phi . c = H₁(c) ) by B2, ORDINAL1:19;
then phi . b in phi . c by B3, A1;
hence phi . b c= phi . c by ORDINAL1:def 2; :: thesis: verum

end;

then ( Union phi is_limes_of phi & H₁(a) = lim phi ) by B1, B2, ThND, ORDINAL2:62;
hence H₁(a) is_limes_of phi by ORDINAL2:def 14; :: thesis: verum

end;

consider b being ordinal number such that
A3: ( a in b & H₁(b) = b ) from ORDINAL5:sch 2(A1, A2);
take b ; :: thesis: ( a in b & b is epsilon )
thus a in b by A3; :: thesis: b is epsilon
thus exp omega ,b = b by A3; :: according to ORDINAL5:def 5 :: thesis: verum