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

A2: now :: thesis: for a being Ordinal st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi

let a be Ordinal; :: thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi )
assume A3: ( not a is empty & a is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal 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 st b in a holds
phi . b = H₁(b) ) implies H₁(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being Ordinal 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; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st b in b & b in dom phi holds
phi . b c= phi . b
let c be Ordinal; :: thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume A5: ( b in c & c in dom phi ) ; :: thesis: phi . b c= phi . c
then ( phi . b = H₁(b) & phi . c = H₁(c) ) by A4, ORDINAL1:10;
then phi . b in phi . c by A5, ORDINAL4:24;
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 A3, A4, Th6, ORDINAL2:45;
hence H₁(a) is_limes_of phi by ORDINAL2:def 10; :: thesis: verum

end;

consider b being Ordinal such that
A6: ( 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 A6; :: thesis: b is epsilon
thus exp (omega,b) = b by A6; :: according to ORDINAL5:def 5 :: thesis: verum