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;
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;