let f be FinSequence of INT ; :: thesis: for m, n being Nat st m >= n holds
f is_non_decreasing_on m,n
let m, n be Nat; :: thesis: ( m >= n implies f is_non_decreasing_on m,n )
assume A1: m >= n ; :: thesis: f is_non_decreasing_on m,n
let i, j be Nat; :: according to FINSEQ_6:def 9 :: thesis: ( m <= i & i <= j & j <= n implies f . i <= f . j )
assume that
A2: ( m <= i & i <= j ) and
A3: j <= n ; :: thesis: f . i <= f . j
A4: m <= j by A2, XXREAL_0:2;

per cases ( m = n or m > n ) by A1, XXREAL_0:1;

suppose m = n ; :: thesis: f . i <= f . j

then j = m by A3, A4, XXREAL_0:1;
hence f . i <= f . j by A2, XXREAL_0:1; :: thesis: verum

end;

suppose m > n ; :: thesis: f . i <= f . j

hence f . i <= f . j by A3, A4, XXREAL_0:2; :: thesis: verum

end;

end;