theorem Th16: :: EXCHSORT:16

for f being Function holds limit- f = sup (dom f)