let f be FinSequence of INT ; 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; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; f is_non_decreasing_on m,n
now for i, j being Nat st m <= i & i <= j & j <= n holds
f . i <= f . jlet i,
j be
Nat;
( m <= i & i <= j & j <= n implies f . b1 <= f . b2 )assume that A6:
m <= i
and A7:
i <= j
and A8:
j <= n
;
f . b1 <= f . b2 end;
hence
f is_non_decreasing_on m,n
by FINSEQ_6:def 9; verum