theorem :: SERIES_2:35

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