deffunc H₁( Ordinal) -> Ordinal = epsilon_ $1;
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
deffunc H₃( Ordinal, Ordinal) -> Ordinal = $2 |^|^ omega;
A1: for b, c being Ordinal holds
( c = H₁(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . 0 = omega |^|^ omega & ( for c being Ordinal st succ c in succ b holds
fi . (succ c) = H₃(c,fi . c) ) & ( for c being Ordinal st c in succ b & c <> 0 & c is limit_ordinal holds
fi . c = H₂(c,fi | c) ) ) ) by Def7;
thus H₁( 0 ) = omega |^|^ omega from ORDINAL2:sch 14(A1); :: thesis: verum