theorem :: SERIES_2:11

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