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;

deffunc H₂( Ordinal, Ordinal) -> set = H₁($2);
deffunc H₃( Ordinal, Ordinal-Sequence) -> set = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: ( 0 in omega implies f . 0 = 1 ) and
A8: for a being Ordinal st succ a in omega holds
f . (succ a) = H₂(a,f . a) and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
f . a = H₃(a,f | a) from ORDINAL2:sch 11();
A9: ( dom f = omega & f . 0 = 1 ) by A6, A7;
A10: for a being Ordinal st a in omega holds
f . (succ a) = H₁(f . a) by A8, ORDINAL1:28;
A11: ( 1 c= Union f & H₁( Union f) = Union f & ( for b being Ordinal st 1 c= b & H₁(b) = b holds
Union f c= b ) ) from ORDINAL5:sch 1(A1, A2, A9, A10);
Union f is epsilon by A11;
then reconsider e = Union f as epsilon Ordinal ;
defpred S₁[ Nat] means f . $1 = omega |^|^ $1;
A12: S₁[ 0 ] by A7, Th13;
A13: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A14: S₁[n] ; :: thesis: S₁[n + 1]
A15: ( Segm (n + 1) = succ (Segm n) & n in omega ) by NAT_1:38, ORDINAL1:def 12;
hence f . (n + 1) = H₁(f . n) by A10
.= omega |^|^ (n + 1) by A14, A15, Th14 ;
:: thesis: verum

end;

A16: for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A13);
then for c being Ordinal st c in omega holds
f . c = omega |^|^ c ;
then A17: omega |^|^ omega = lim f by A6, Th15;
f is non-decreasing

proof

let a be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st a in b & b in dom f holds
f . a c= f . b
let b be Ordinal; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
assume A18: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then reconsider n = a, m = b as Element of omega by A6, ORDINAL1:10;
a c= b by A18, ORDINAL1:def 2;
then omega |^|^ a c= omega |^|^ b by Th21;
then f . n c= omega |^|^ m by A16;
hence f . a c= f . b by A16; :: thesis: verum

end;

then e is_limes_of f by A6, Th6;
then A19: omega |^|^ omega = e by A17, ORDINAL2:def 10;
A20: succ 0 = 1 ;
then A21: 0 in 1 by ORDINAL1:6;

now :: thesis: for b being epsilon Ordinal st 0 in b holds
e c= b

let b be epsilon Ordinal; :: thesis: ( 0 in b implies e c= b )
assume 0 in b ; :: thesis: e c= b
then ( 1 c= b & H₁(b) = b ) by A20, Def5, ORDINAL1:21;
hence e c= b by A11; :: thesis: verum

end;

hence first_epsilon_greater_than 0 = omega |^|^ omega by A19, A21, Def6, A11; :: thesis: verum