theorem :: SERIES_4:19

for a being Real
for s being Real_Sequence st a <> 1 & ( for n being Nat holds s . n = n * (a |^ n) ) holds
for n being Nat holds (Partial_Sums s) . n = ((a * (1 - (a |^ n))) / ((1 - a) |^ 2)) - ((n * (a |^ (n + 1))) / (1 - a))