theorem :: SERIES_2:31

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