theorem :: SERIES_2:28

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