theorem :: SERIES_2:19

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