theorem :: SERIES_4:17

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