theorem :: SERIES_2:21

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