for f being sequence of NAT st ( for n being Nat holds f . (n + 1) <= f . n ) holds
ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m