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;

deffunc H₂( Ordinal, Ordinal) -> set = H₁($2);
deffunc H₃( Ordinal, Ordinal-Sequence) -> set = lim $2;
consider f being Ordinal-Sequence such that
A4: dom f = omega and
A5: ( {} in omega implies f . {} = 1 ) and
A6: for a being ordinal number st succ a in omega holds
f . (succ a) = H₂(a,f . a) and
for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
f . a = H₃(a,f | a) from ORDINAL2:sch 11();
F1: ( dom f = omega & f . 0 = 1 ) by A4, A5;

F2: now

let a be ordinal number ; :: thesis: ( a in omega implies f . (succ a) = H₁(f . a) )
assume a in omega ; :: thesis: f . (succ a) = H₁(f . a)
then succ a in omega by ORDINAL1:41;
hence f . (succ a) = H₁(f . a) by A6; :: thesis: verum

end;

A7: ( 1 c= Union f & H₁( Union f) = Union f & ( for b being ordinal number st 1 c= b & H₁(b) = b holds
Union f c= b ) ) from ORDINAL5:sch 1(A1, A2, F1, F2);
Union f is epsilon

proof

thus H₁( Union f) = Union f by A7; :: according to ORDINAL5:def 5 :: thesis: verum

end;

then reconsider e = Union f as epsilon Ordinal ;
defpred S₁[ Nat] means f . $1 = omega |^|^ $1;
I1: S₁[ 0 ] by F1, Th0;
I2: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume I3: S₁[n] ; :: thesis: S₁[n + 1]
I4: ( n + 1 = succ n & n in omega ) by NAT_1:39, ORDINAL1:def 13;
hence f . (n + 1) = H₁(f . n) by F2
.= omega |^|^ (n + 1) by I3, I4, Th1 ;
:: thesis: verum

end;

A8: for n being natural number holds S₁[n] from NAT_1:sch 2(I1, I2);
then for c being ordinal number st c in omega holds
f . c = omega |^|^ c ;
then A9: omega |^|^ omega = lim f by F1, Th2;
f is non-decreasing

proof

let a be ordinal number ; :: according to ORDINAL5:def 2 :: thesis: for b being ordinal number st a in b & b in dom f holds
f . a c= f . b
let b be ordinal number ; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
assume B1: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then reconsider n = a, m = b as Element of omega by F1, ORDINAL1:19;
a c= b by B1, ORDINAL1:def 2;
then omega |^|^ a c= omega |^|^ b by Th5;
then f . n c= omega |^|^ m by A8;
hence f . a c= f . b by A8; :: thesis: verum

end;

then e is_limes_of f by F1, ThND;
then AA: omega |^|^ omega = e by A9, ORDINAL2:def 14;
B2: succ 0 = 1 ;
then 0 in 1 by ORDINAL1:10;
then AB: 0 in e by A7;

now

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 B2, EPSILON, ORDINAL1:33;
hence e c= b by A7; :: thesis: verum

end;

hence first_epsilon_greater_than 0 = omega |^|^ omega by AA, AB, FEGT; :: thesis: verum