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