theorem Th20: :: EXCHSORT:20

for f being Function holds base- f = inf (dom f)