:: deftheorem Def4 defines base- EXCHSORT:def 4 :
for f being Function
for b₂ being Ordinal holds
( ( ex a being Ordinal st a in dom f implies ( b₂ = base- f iff f is b₂ -based ) ) & ( ( for a being Ordinal holds not a in dom f ) implies ( b₂ = base- f iff b₂ = 0 ) ) );