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;

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;