theorem :: SERIES_4:13

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