theorem :: SERIES_2:41

for a, b being Real
for s being Real_Sequence st ( for n being Nat holds s . n = (a * n) + b ) holds
for n being Nat holds (Partial_Sums s) . n = ((((a * (n + 1)) * n) / 2) + (n * b)) + b by Lm14;