theorem Th52: :: SERIES_5:52

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