let f be non-increasing FinSequence of REAL ; for n being Element of NAT holds f /^ n is non-increasing
let n be Nat; ( n is Element of NAT implies f /^ n is non-increasing )
set fn = f /^ n;
now for m being Nat st m in dom (f /^ n) & m + 1 in dom (f /^ n) holds
(f /^ n) . m >= (f /^ n) . (m + 1)let m be
Nat;
( m in dom (f /^ n) & m + 1 in dom (f /^ n) implies (f /^ n) . m >= (f /^ n) . (m + 1) )assume that A1:
m in dom (f /^ n)
and A2:
m + 1
in dom (f /^ n)
;
(f /^ n) . m >= (f /^ n) . (m + 1)A3:
m <= m + n
by NAT_1:11;
1
<= m
by A1, FINSEQ_3:25;
then A4:
1
<= m + n
by A3, XXREAL_0:2;
A5:
1
<= (m + n) + 1
by NAT_1:11;
A6:
m + 1
<= len (f /^ n)
by A2, FINSEQ_3:25;
set r =
(f /^ n) . m;
set s =
(f /^ n) . (m + 1);
A7:
(m + 1) + n = (m + n) + 1
;
A8:
m <= len (f /^ n)
by A1, FINSEQ_3:25;
now ( ( n <= len f & (f /^ n) . m >= (f /^ n) . (m + 1) ) or ( len f < n & (f /^ n) . m >= (f /^ n) . (m + 1) ) )per cases
( n <= len f or len f < n )
;
case A9:
n <= len f
;
(f /^ n) . m >= (f /^ n) . (m + 1)then A10:
len (f /^ n) = (len f) - n
by Def1;
then
m + n <= len f
by A8, XREAL_1:19;
then A11:
m + n in dom f
by A4, FINSEQ_3:25;
(m + n) + 1
<= len f
by A6, A7, A10, XREAL_1:19;
then A12:
(m + n) + 1
in dom f
by A5, FINSEQ_3:25;
(
(f /^ n) . m = f . (m + n) &
(f /^ n) . (m + 1) = f . ((m + n) + 1) )
by A1, A2, A7, A9, Def1;
hence
(f /^ n) . m >= (f /^ n) . (m + 1)
by A11, A12, Def3;
verum end; hence
(f /^ n) . m >= (f /^ n) . (m + 1)
;
verum end;
hence
( n is Element of NAT implies f /^ n is non-increasing )
; verum