theorem :: SERIES_2:24

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