let f be FinSequence of INT ; :: thesis: for m, k1, k, n being Nat st k1 = k - 1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k + 1,n & ( for i being Nat st m <= i & i < k holds
f . i <= f . k ) & ( for i being 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 Nat; :: thesis: ( k1 = k - 1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k + 1,n & ( for i being Nat st m <= i & i < k holds
f . i <= f . k ) & ( for i being Nat st k < i & i <= n holds
f . k <= f . i ) implies f is_non_decreasing_on m,n )
assume A1: 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 Nat st
( m <= i & i < k & not f . i <= f . k ) or ex i being 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 Nat st
( m <= i & i < k & not f . i <= f . k ) or ex i being 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 Nat st
( m <= i & i < k & not f . i <= f . k ) or ex i being Nat st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A4: for i being Nat st m <= i & i < k holds
f . i <= f . k ; :: thesis: ( ex i being Nat st
( k < i & i <= n & not f . k <= f . i ) or f is_non_decreasing_on m,n )
assume A5: for i being Nat st k < i & i <= n holds
f . k <= f . i ; :: thesis: f is_non_decreasing_on m,n
now :: thesis: for i, j being Nat st m <= i & i <= j & j <= n holds
f . i <= f . j
let i, j be Nat; :: thesis: ( m <= i & i <= j & j <= n implies f . b1 <= f . b2 )
assume that
A6: m <= i and
A7: i <= j and
A8: j <= n ; :: thesis: f . b1 <= f . b2
per cases ( j < k or j = k or j > k ) by XXREAL_0:1;
suppose j < k ; :: thesis: f . b1 <= f . b2
then j + 1 <= k by INT_1:7;
then j <= k1 by A1, XREAL_1:19;
hence f . i <= f . j by A2, A6, A7, FINSEQ_6:def 9; :: thesis: verum
end;
suppose A9: j = k ; :: thesis: f . b1 <= f . b2
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f . b1 <= f . b2
hence f . i <= f . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f . b1 <= f . b2
then i < j by A7, XXREAL_0:1;
hence f . i <= f . j by A4, A6, A9; :: thesis: verum
end;
end;
end;
suppose A10: j > k ; :: thesis: f . b1 <= f . b2
per cases ( i < k or i = k or i > k ) by XXREAL_0:1;
suppose i < k ; :: thesis: f . b1 <= f . b2
then A11: f . k >= f . i by A4, A6;
f . j >= f . k by A5, A8, A10;
hence f . i <= f . j by A11, XXREAL_0:2; :: thesis: verum
end;
suppose A12: i = k ; :: thesis: f . b1 <= f . b2
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f . b1 <= f . b2
hence f . i <= f . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f . b1 <= f . b2
then i < j by A7, XXREAL_0:1;
hence f . i <= f . j by A5, A8, A12; :: thesis: verum
end;
end;
end;
suppose i > k ; :: thesis: f . b1 <= f . b2
then i >= k + 1 by INT_1:7;
hence f . i <= f . j by A3, A7, A8, FINSEQ_6:def 9; :: thesis: verum
end;
end;
end;
end;
end;
hence f is_non_decreasing_on m,n by FINSEQ_6:def 9; :: thesis: verum