let n be Nat; :: thesis: for f being nonnegative-yielding FinSequence of REAL holds Sum f >= f . n
let f be nonnegative-yielding FinSequence of REAL ; :: thesis: Sum f >= f . n

per cases ( not n in dom f or n in dom f ) ;

suppose not n in dom f ; :: thesis: Sum f >= f . n

hence Sum f >= f . n by FUNCT_1:def 2; :: thesis: verum

end;

suppose A0: n in dom f ; :: thesis: Sum f >= f . n

then A0a: ( len f >= n & n >= 1 ) by FINSEQ_3:25;
then reconsider k = n - 1 as Nat ;
A0b: k + 1 >= k + 0 by XREAL_1:6;
A0c: (f | n) . n = f . n by A0, A0a, NEWTON02:107;
A1: f | (k + 1) = ((f | (k + 1)) | k) ^ <*((f | (k + 1)) . (k + 1))*> by RFINSEQ:7, A0, NEWTON02:110
.= (f | k) ^ <*(f . (k + 1))*> by FINSEQ_1:82, A0b, A0c ;
A2: Sum f = Sum (((f | k) ^ <*(f . (k + 1))*>) ^ (f /^ n)) by A1, RFINSEQ:8
.= (Sum ((f | k) ^ <*(f . (k + 1))*>)) + (Sum (f /^ n)) by RVSUM_1:75
.= ((Sum (f | k)) + (f . (k + 1))) + (Sum (f /^ n)) by RVSUM_1:74 ;
(f . (k + 1)) + ((Sum (f | k)) + (Sum (f /^ n))) >= (f . (k + 1)) + 0 by XREAL_1:6;
hence Sum f >= f . n by A2; :: thesis: verum

end;

end;