deffunc H₁( Ordinal) -> Ordinal = epsilon_ a;
defpred S₁[ Ordinal] means H₁(a) is epsilon ;
A1: S₁[ 0 ] by Th36, Th41;
A2: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: 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 Th40
.= epsilon_ (succ b) by Th42 ;
hence S₁[ succ b] ; :: thesis: verum

end;

A3: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A4: ( b <> 0 & b is limit_ordinal ) and
A5: for c being Ordinal st c in b holds
S₁[c] ; :: thesis: S₁[b]
consider f being Ordinal-Sequence such that
A6: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
A7: H₁(b) = Union f by A4, A6, Th46;
set X = rng f;
0 in b by A4, ORDINAL3:8;
then f . 0 in rng f by A6, FUNCT_1:def 3;
then reconsider X = rng f as non empty set ;

A8: now :: thesis: for x being object st x in X holds
x is epsilon Ordinal

let x be object ; :: thesis: ( x in X implies x is epsilon Ordinal )
assume x in X ; :: thesis: x is epsilon Ordinal
then consider a being object such that
A9: ( a in dom f & f . a = x ) by FUNCT_1:def 3;
reconsider a = a as Ordinal by A9;
x = H₁(a) by A6, A9;
hence x is epsilon Ordinal by A5, A6, A9; :: thesis: verum

end;

now :: thesis: for x being Ordinal st x in X holds
first_epsilon_greater_than x in X

let x be Ordinal; :: thesis: ( x in X implies first_epsilon_greater_than x in X )
assume A10: x in X ; :: thesis: first_epsilon_greater_than x in X
then consider a being object such that
A11: ( a in dom f & f . a = x ) by FUNCT_1:def 3;
reconsider a = a as Ordinal by A11;
A12: succ a in b by A4, A6, A11, ORDINAL1:28;
reconsider e = x as epsilon Ordinal by A8, A10;
e = H₁(a) by A6, A11;
then first_epsilon_greater_than e = H₁(a) |^|^ omega by Th40
.= H₁( succ a) by Th42
.= f . (succ a) by A6, A12 ;
hence first_epsilon_greater_than x in X by A6, A12, FUNCT_1:def 3; :: thesis: verum

end;

hence S₁[b] by A7, A8, Th50; :: thesis: verum

end;

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