let f be FinSequence of INT ; :: thesis: for k being Element of NAT holds f is_non_decreasing_on k,k
let k be Element of NAT ; :: thesis: f is_non_decreasing_on k,k

now

let i, j be Element of NAT ; :: thesis: ( k <= i & i <= j & j <= k implies f . i <= f . j )
assume that
A1: ( k <= i & i <= j ) and
A2: j <= k ; :: thesis: f . i <= f . j
k <= j by A1, XXREAL_0:2;
then j = k by A2, XXREAL_0:1;
hence f . i <= f . j by A1, XXREAL_0:1; :: thesis: verum

end;

hence f is_non_decreasing_on k,k by GRAPH_2:def 13; :: thesis: verum