let A be Ordinal; :: thesis:
defpred S₁[ Ordinal] means 0 +^ $1 = $1;
A1: for A being Ordinal st S₁[A] holds
S₁[ succ A] by Th28;
A2: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

deffunc H₁( Ordinal) -> Ordinal = 0 +^ $1;
let A be Ordinal; :: thesis:
assume that
A3: ( A <> 0 & A is limit_ordinal ) and
A4: for B being Ordinal st B in A holds
0 +^ B = B ; :: thesis:
consider fi being Ordinal-Sequence such that
A5: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
A6: rng fi = A

let x be object ; :: thesis:
assume x in rng fi ; :: thesis:
then consider y being object such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A7;
x = 0 +^ y by A5, A7, A8
.= y by A4, A5, A7 ;
hence x in A by A5, A7; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in A ; :: thesis:
then reconsider B = x as Ordinal ;
( 0 +^ B = B & fi . B = 0 +^ B ) by A4, A5, A9;
hence x in rng fi by A5, A9, FUNCT_1:def 3; :: thesis:

end;

0 +^ A = sup fi by A3, A5, Th29
.= sup (rng fi) ;
hence S₁[A] by A6, Th18; :: thesis:

end;