theorem :: SERIES_4:12

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