theorem :: SERIES_2:25

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