theorem :: SERIES_4:28

for a being Real
for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = a / n & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n = (a |^ n) / (n !)