theorem :: EXCHSORT:17

for f being Function holds f is limit- f -limited by Th16;