let f be FinSequence of INT ; :: thesis: for m, n being Element of NAT st m >= n holds
f is_non_decreasing_on m,n
let m, n be Element of 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 Element of NAT ; :: according to GRAPH_2:def 12 :: thesis: ( m <= i & i <= j & j <= n implies f . i <= f . j )
assume that
B1: ( m <= i & i <= j ) and
B2: j <= n ; :: thesis: f . i <= f . j
B3: m <= j by B1, 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 B2, B3, XXREAL_0:1;
hence f . i <= f . j by B1, XXREAL_0:1; :: thesis: verum

end;

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

hence f . i <= f . j by B2, B3, XXREAL_0:2; :: thesis: verum

end;

end;