theorem :: SERIES_1:15

for s being Real_Sequence st s is summable holds
for n being Nat holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))