:: deftheorem Def7 defines epsilon_ ORDINAL5:def 7 :
for a, b₂ being Ordinal holds
( b₂ = epsilon_ a iff ex phi being Ordinal-Sequence st
( b₂ = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );