theorem :: SERIES_4:10

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