theorem :: SERIES_4:18

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