theorem Th24: :: EXCHSORT:24

for f being Sequence holds
( base- f = 0 & limit- f = dom f & len- f = dom f )