let a be ordinal number ; :: 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 number holds
( c = H₁(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = omega |^|^ omega & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H₃(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H₂(c,fi | c) ) ) ) by EPSILON2;
for b being ordinal number holds H₁( succ b) = H₃(b,H₁(b)) from ORDINAL2:sch 15(A1);
hence epsilon_ (succ a) = (epsilon_ a) |^|^ omega ; :: thesis: verum