theorem :: SERIES_2:16

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = ((2 * n) - 1) |^ 3 & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = (n |^ 2) * ((2 * (n |^ 2)) - 1)