theorem PartialNonneg: :: PRIMRECI:6

for n being Nat
for s being Real_Sequence st ( for n being Nat holds 0 <= s . n ) holds
0 <= (Partial_Sums s) . n