theorem Th27: :: EXCHSORT:27

for f being Sequence st f is descending & f . 0 is finite holds
f is finite