theorem :: SERIES_2:37

for s being Real_Sequence st ( for n being Nat holds s . n = (n !) * n ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = ((n + 1) !) - 1