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