let a be Ordinal; :: thesis: epsilon_ (succ a) = (epsilon_ a) |^|^ omega
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;
for b being Ordinal holds H₁( succ b) = H₃(b,H₁(b)) from ORDINAL2:sch 15(A1);
hence epsilon_ (succ a) = (epsilon_ a) |^|^ omega ; :: thesis: verum