deffunc H₁( Ordinal) -> Ordinal = epsilon_ a;
defpred S₁[ Ordinal] means H₁(a) is epsilon ;
A0: S₁[ {} ] by Th20, Th30;
A1: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume S₁[b] ; :: thesis: S₁[ succ b]
then first_epsilon_greater_than (epsilon_ b) = (epsilon_ b) |^|^ omega by Th24
.= epsilon_ (succ b) by Th31 ;
hence S₁[ succ b] ; :: thesis: verum

end;

A2: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) implies S₁[b] )
assume that
Z0: ( b <> {} & b is limit_ordinal ) and
Z1: for c being ordinal number st c in b holds
S₁[c] ; :: thesis: S₁[b]
consider f being Ordinal-Sequence such that
Z2: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
Z3: H₁(b) = Union f by Z0, Z2, Th35;
set X = rng f;
0 in b by Z0, ORDINAL3:10;
then f . 0 in rng f by Z2, FUNCT_1:def 5;
then reconsider X = rng f as non empty set ;

Z4: now

let x be set ; :: thesis: ( x in X implies x is epsilon Ordinal )
assume x in X ; :: thesis: x is epsilon Ordinal
then consider a being set such that
Z5: ( a in dom f & f . a = x ) by FUNCT_1:def 5;
reconsider a = a as Ordinal by Z5;
x = H₁(a) by Z2, Z5;
hence x is epsilon Ordinal by Z1, Z2, Z5; :: thesis: verum

end;

now

let x be Ordinal; :: thesis: ( x in X implies first_epsilon_greater_than x in X )
assume Z6: x in X ; :: thesis: first_epsilon_greater_than x in X
then consider a being set such that
Z5: ( a in dom f & f . a = x ) by FUNCT_1:def 5;
reconsider a = a as Ordinal by Z5;
Z7: succ a in b by Z0, Z2, Z5, ORDINAL1:41;
reconsider e = x as epsilon Ordinal by Z4, Z6;
e = H₁(a) by Z2, Z5;
then first_epsilon_greater_than e = H₁(a) |^|^ omega by Th24
.= H₁( succ a) by Th31
.= f . (succ a) by Z2, Z7 ;
hence first_epsilon_greater_than x in X by Z2, Z7, FUNCT_1:def 5; :: thesis: verum

end;

hence S₁[b] by Z3, Z4, Th36; :: thesis: verum

end;

for a being ordinal number holds S₁[a] from ORDINAL2:sch 1(A0, A1, A2);
hence epsilon_ a is epsilon ; :: thesis: verum