theorem :: SERIES_2:18

for s being Real_Sequence st ( for n being Nat holds s . n = ((- 1) |^ (n + 1)) * (n |^ 4) ) holds
for n being Nat holds (Partial_Sums s) . n = (((((- 1) |^ (n + 1)) * n) * (n + 1)) * (((n |^ 2) + n) - 1)) / 2