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