theorem :: EXCHSORT:28

for f being Sequence st f is descending & f . 0 is finite & ( for a being Ordinal st f . a <> {} holds
succ a in dom f ) holds
last f = {}