theorem :: SERIES_2:23

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