theorem :: SERIES_2:15

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