theorem :: SERIES_2:30

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