theorem :: SERIES_2:26

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