:: deftheorem defines is_non_decreasing_on FINSEQ_6:def 9 :
for F being FinSequence of INT
for m, n being Nat holds
( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds
F . i <= F . j );