theorem Th22: :: SERIES_1:22

for n being Nat
for a being Real st a <> 1 holds
(Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a)