theorem :: SERIES_2:17

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