let f be non-increasing FinSequence of REAL ; :: thesis: for n being Nat holds f | n is non-increasing FinSequence of REAL
let n be Nat; :: thesis:
set fn = f | n;
now :: thesis: ( ( n = 0 & f | n is non-increasing FinSequence of REAL ) or ( n <> 0 & f | n is non-increasing FinSequence of REAL ) )
per cases ( n = 0 or n <> 0 ) ;
case n <> 0 ; :: thesis:
then 0 < n ;
then A1: 0 + 1 <= n by NAT_1:13;
now :: thesis: ( ( len f <= n & f | n is non-increasing FinSequence of REAL ) or ( n < len f & f | n is non-increasing FinSequence of REAL ) )
per cases ( len f <= n or n < len f ) ;
case n < len f ; :: thesis:
then A2: ( n in dom f & len (f | n) = n ) by ;
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) )
A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def 3;
assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; :: thesis: (f | n) . m >= (f | n) . (m + 1)
then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, Th6;
( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, Th6;
hence (f | n) . m >= (f | n) . (m + 1) by ; :: thesis: verum
end;
hence f | n is non-increasing FinSequence of REAL by Def3; :: thesis: verum
end;
end;
end;
hence f | n is non-increasing FinSequence of REAL ; :: thesis: verum
end;
end;
end;
hence f | n is non-increasing FinSequence of REAL ; :: thesis: verum