theorem :: EXCHSORT:10

for a being Ordinal
for f being Function holds
( ( f is a -based & f is segmental ) iff ex b being Ordinal st
( dom f = b \ a & a c= b ) )