theorem :: SERIES_2:5

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