let f be FinSequence of INT ; :: thesis: for m, k1, k, n being Element of NAT st m <= k & k <= n & k1 = k - 1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k + 1,n & ( for i being Element of NAT st m <= i & i < k holds
f . i <= f . k ) & ( for i being Element of NAT st k < i & i <= n holds
f . k <= f . i ) holds
f is_non_decreasing_on m,n
let m, k1, k, n be Element of NAT ; :: thesis: ( m <= k & k <= n & k1 = k - 1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k + 1,n & ( for i being Element of NAT st m <= i & i < k holds
f . i <= f . k ) & ( for i being Element of NAT st k < i & i <= n holds
f . k <= f . i ) implies f is_non_decreasing_on m,n )
assume A1: ( m <= k & k <= n & k1 = k - 1 ) ; :: thesis: ( not f is_non_decreasing_on m,k1 or not f is_non_decreasing_on k + 1,n or ex i being Element of NAT st
( m <= i & i < k & not f . i <= f . k ) or ex i being Element of NAT st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A2: f is_non_decreasing_on m,k1 ; :: thesis: ( not f is_non_decreasing_on k + 1,n or ex i being Element of NAT st
( m <= i & i < k & not f . i <= f . k ) or ex i being Element of NAT st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A3: f is_non_decreasing_on k + 1,n ; :: thesis: ( ex i being Element of NAT st
( m <= i & i < k & not f . i <= f . k ) or ex i being Element of NAT st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A4: for i being Element of NAT st m <= i & i < k holds
f . i <= f . k ; :: thesis: ( ex i being Element of NAT st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A5: for i being Element of NAT st k < i & i <= n holds
f . k <= f . i ; :: thesis: f is_non_decreasing_on m,n

now

let i, j be Element of NAT ; :: thesis: ( m <= i & i <= j & j <= n implies f . b₁ <= f . b₂ )
assume A6: ( m <= i & i <= j & j <= n ) ; :: thesis: f . b₁ <= f . b₂

per cases ( j < k or j = k or j > k ) by XXREAL_0:1;

suppose j < k ; :: thesis: f . b₁ <= f . b₂

then j + 1 <= k by INT_1:20;
then j <= k1 by A1, XREAL_1:21;
hence f . i <= f . j by A2, A6, GRAPH_2:def 13; :: thesis: verum

end;

suppose A7: j = k ; :: thesis: f . b₁ <= f . b₂

hereby :: thesis: verum

per cases ( i = j or i <> j ) ;

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

hence f . i <= f . j ; :: thesis: verum

end;

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

then i < j by A6, XXREAL_0:1;
hence f . i <= f . j by A4, A6, A7; :: thesis: verum

end;

end;

end;

end;

suppose A8: j > k ; :: thesis: f . b₁ <= f . b₂

hereby :: thesis: verum

per cases ( i < k or i = k or i > k ) by XXREAL_0:1;

suppose A9: i < k ; :: thesis: f . i <= f . j

A10: f . j >= f . k by A5, A6, A8;
f . k >= f . i by A4, A6, A9;
hence f . i <= f . j by A10, XXREAL_0:2; :: thesis: verum

end;

suppose A11: i = k ; :: thesis: f . i <= f . j

hereby :: thesis: verum

per cases ( i = j or i <> j ) ;

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

hence f . i <= f . j ; :: thesis: verum

end;

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

then i < j by A6, XXREAL_0:1;
hence f . i <= f . j by A5, A6, A11; :: thesis: verum

end;

end;

end;

end;

suppose i > k ; :: thesis: f . i <= f . j

then i >= k + 1 by INT_1:20;
hence f . i <= f . j by A3, A6, GRAPH_2:def 13; :: thesis: verum

end;

end;

end;

end;

end;

end;

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