theorem Th11: :: SERIES_1:11

for s, s1 being Real_Sequence st ( for n being Nat holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1