theorem :: SERIES_4:14

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