theorem :: SERIES_4:23

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