theorem :: EXCHSORT:21

for f being Function holds f is base- f -based