theorem Th36: :: SERIES_3:36

for s, s1 being Real_Sequence st s = s1 (#) s1 holds
for n being Nat holds (Partial_Sums s) . n >= 0