for f being Real_Sequence
for N being Nat st ( for n being Nat st n >= N holds
f . n <= f . (n + 1) ) holds
for n, m being Nat st N <= n & n <= m holds
f . n <= f . m