:: deftheorem defines non-increasing ORDINAL5:def 3 :
for f being Sequence holds
( f is non-increasing iff for a, b being Ordinal st a in b & b in dom f holds
f . b c= f . a );