let n be Nat; :: thesis: for f being real-valued nonnegative-yielding FinSequence holds Sum f >= f . n
let f be real-valued nonnegative-yielding FinSequence; :: 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 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 ;
k + 1 > k + 0 by XREAL_1:6;
then len f > k by A0a, XXREAL_0:2;
then A1: f | (k + 1) = (f | k) ^ <*(f . (k + 1))*> by FINSEQ_5:83;
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;