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