theorem :: EXCHSORT:25

for f being finite array st ( for a being Ordinal st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) holds
f is descending