theorem :: SERIES_2:20

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