let f be non-increasing FinSequence of REAL ; :: thesis: for n being Element of NAT holds f /^ n is non-increasing
let n be Nat; :: thesis: ( n is Element of NAT implies f /^ n is non-increasing )
set fn = f /^ n;
now :: thesis: 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; :: thesis: ( 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) ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
A3: m <= m + n by NAT_1:11;
1 <= m by ;
then A4: 1 <= m + n by ;
A5: 1 <= (m + n) + 1 by NAT_1:11;
A6: m + 1 <= len (f /^ n) by ;
set r = (f /^ n) . m;
set s = (f /^ n) . (m + 1);
A7: (m + 1) + n = (m + n) + 1 ;
A8: m <= len (f /^ n) by ;
now :: thesis: ( ( 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 ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
then A10: len (f /^ n) = (len f) - n by Def1;
then m + n <= len f by ;
then A11: m + n in dom f by ;
(m + n) + 1 <= len f by ;
then A12: (m + n) + 1 in dom f by ;
( (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 ; :: thesis: verum
end;
case len f < n ; :: thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
then f /^ n = <*> REAL by Def1;
hence (f /^ n) . m >= (f /^ n) . (m + 1) ; :: thesis: verum
end;
end;
end;
hence (f /^ n) . m >= (f /^ n) . (m + 1) ; :: thesis: verum
end;
hence ( n is Element of NAT implies f /^ n is non-increasing ) ; :: thesis: verum