theorem PartialLeSum: :: PRIMRECI:7

for i being Nat
for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
(Partial_Sums s) . i <= Sum s