theorem :: SERIES_4:26

for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n = 1 / (n + 1) ) holds
(Partial_Product s) . n = 1 / ((n + 1) !)