deffunc H1( Ordinal) -> set = exp (omega,$1);
A1: for a, b being Ordinal st a in b holds
H1(a) in H1(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 = H1(b) ) holds
H1(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 = H1(b) ) holds
H1(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 = H1(b) ) holds
H1(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 = H1(b) ) implies H1(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H1(b) ) ) ; :: thesis: H1(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 = H1(b) & phi . c = H1(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 & H1(a) = lim phi ) by A3, A4, Th6, ORDINAL2:45;
hence H1(a) is_limes_of phi by ORDINAL2:def 10; :: thesis: verum
end;
deffunc H2( Ordinal, Ordinal) -> set = H1($2);
deffunc H3( 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) = H2(a,f . a) and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
f . a = H3(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) = H1(f . a) by A8, ORDINAL1:28;
A11: ( 1 c= Union f & H1( Union f) = Union f & ( for b being Ordinal st 1 c= b & H1(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 S1[ Nat] means f . $1 = omega |^|^ $1;
A12: S1[ 0 ] by A7, Th13;
A13: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A14: S1[n] ; :: thesis: S1[n + 1]
A15: ( Segm (n + 1) = succ (Segm n) & n in omega ) by NAT_1:38, ORDINAL1:def 12;
hence f . (n + 1) = H1(f . n) by A10
.= omega |^|^ (n + 1) by A14, A15, Th14 ;
:: thesis: verum
end;
A16: for n being Nat holds S1[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 & H1(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