theorem :: SERIES_2:36

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