theorem Th26: :: EXCHSORT:26

for f being array st len- f = omega & ( 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