for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))