theorem :: SERIES_2:6

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