:: deftheorem Def5 defines limit- EXCHSORT:def 5 :
for f being Function
for b₂ being Ordinal holds
( ( ex a being Ordinal st a in dom f implies ( b₂ = limit- f iff f is b₂ -limited ) ) & ( ( for a being Ordinal holds not a in dom f ) implies ( b₂ = limit- f iff b₂ = 0 ) ) );