for b being Ordinal
for f being Function holds
( ( f is b -limited & not f is empty & f is segmental ) iff ex a being Ordinal st
( dom f = b \ a & a in b ) )