theorem :: SERIES_2:39

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