let Omega be non empty set ; :: thesis: 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))

let Sigma be SigmaField of Omega; :: thesis: 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))

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))

let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))
let n be Nat; :: thesis: (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))
defpred S1[ Nat] means exp_R . (- ((Partial_Sums (Prob * A)) . \$1)) = (Partial_Product (JSum (Prob * A))) . \$1;
A1: exp_R . (- ((Partial_Sums (Prob * A)) . 0)) = exp_R . (- ((Prob * A) . 0)) by SERIES_1:def 1;
(Partial_Product (JSum (Prob * A))) . 0 = (JSum (Prob * A)) . 0 by SERIES_3:def 1;
then (Partial_Product (JSum (Prob * A))) . 0 = Sum ((- ((Prob * A) . 0)) rExpSeq) by Def1;
then A2: S1[ 0 ] by ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
A5: (Partial_Product (JSum (Prob * A))) . (k + 1) = ((Partial_Product (JSum (Prob * A))) . k) * ((JSum (Prob * A)) . (k + 1)) by SERIES_3:def 1;
A6: (Partial_Product (JSum (Prob * A))) . (k + 1) = (exp_R . (- ((Partial_Sums (Prob * A)) . k))) * (Sum ((- ((Prob * A) . (k + 1))) rExpSeq)) by A4, A5, Def1;
A7: (exp_R (- ((Partial_Sums (Prob * A)) . k))) * (exp_R (- ((Prob * A) . (k + 1)))) = exp_R ((- ((Partial_Sums (Prob * A)) . k)) + (- ((Prob * A) . (k + 1)))) by SIN_COS:50;
- (((Partial_Sums (Prob * A)) . k) + ((Prob * A) . (k + 1))) = - ((Partial_Sums (Prob * A)) . (k + 1)) by SERIES_1:def 1;
hence S1[k + 1] by ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
hence (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n)) ; :: thesis: verum