let f be FinSequence of REAL ; ( ( for k being Nat st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) implies f is decreasing )
assume A1:
for k being Nat st 1 <= k & k < len f holds
f /. k > f /. (k + 1)
; f is decreasing
now for i, j being Element of NAT st i in dom f & j in dom f & i < j holds
f . i > f . jlet i,
j be
Element of
NAT ;
( i in dom f & j in dom f & i < j implies f . i > f . j )now ( i in dom f & j in dom f & i < j implies f . i > f . j )defpred S1[
Nat]
means (
i + (1 + $1) <= len f implies
f /. i > f /. (i + (1 + $1)) );
assume that A2:
i in dom f
and A3:
j in dom f
and A4:
i < j
;
f . i > f . jA5:
1
<= i
by A2, FINSEQ_3:25;
A6:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A7:
(
i + (1 + k) <= len f implies
f /. i > f /. (i + (1 + k)) )
;
S1[k + 1]
hence
S1[
k + 1]
;
verum
end;
i + 1
<= j
by A4, NAT_1:13;
then
j -' (i + 1) = j - (i + 1)
by XREAL_1:233;
then A12:
i + (1 + (j -' (i + 1))) = j
;
A13:
f /. i = f . i
by A2, PARTFUN1:def 6;
A14:
j <= len f
by A3, FINSEQ_3:25;
then
i < len f
by A4, XXREAL_0:2;
then A15:
S1[
0 ]
by A1, A5;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A15, A6);
then
f /. i > f /. j
by A14, A12;
hence
f . i > f . j
by A3, A13, PARTFUN1:def 6;
verum end; hence
(
i in dom f &
j in dom f &
i < j implies
f . i > f . j )
;
verum end;
hence
f is decreasing
; verum