theorem :: SERIES_2:14

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