theorem :: SERIES_2:27

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