let f be real-valued non-decreasing FinSequence; :: thesis: for n being Nat holds f | n is non-decreasing FinSequence of REAL
let n be Nat; :: thesis: f | n is non-decreasing FinSequence of REAL
reconsider f = f as non-decreasing FinSequence of REAL by RVSUM_1:145;
set fn = f | n;
now :: thesis: ( ( n = 0 & f | n is non-decreasing FinSequence of REAL ) or ( n <> 0 & f | n is non-decreasing FinSequence of REAL ) )
per cases ( n = 0 or n <> 0 ) ;
case n <> 0 ; :: thesis: f | n is non-decreasing FinSequence of REAL
then A1: 0 + 1 <= n by NAT_1:13;
now :: thesis: ( ( len f <= n & f | n is non-decreasing FinSequence of REAL ) or ( n < len f & f | n is non-decreasing FinSequence of REAL ) )
per cases ( len f <= n or n < len f ) ;
case n < len f ; :: thesis: f | n is non-decreasing FinSequence of REAL
then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:59, FINSEQ_3:25;
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, RFINSEQ:6;
( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, RFINSEQ:6;
hence (f | n) . m <= (f | n) . (m + 1) by A5, INTEGRA2:def 1; :: thesis: verum
end;
hence f | n is non-decreasing FinSequence of REAL by INTEGRA2:def 1; :: thesis: verum
end;
end;
end;
hence f | n is non-decreasing FinSequence of REAL ; :: thesis: verum
end;
end;
end;
hence f | n is non-decreasing FinSequence of REAL ; :: thesis: verum