theorem :: SERIES_2:29

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