theorem :: SERIES_2:33

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