:: deftheorem defines len- EXCHSORT:def 6 :
for f being Function holds len- f = (limit- f) -^ (base- f);