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 Element of 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 Element of 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 Element of 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 Element of NAT holds (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))
let n be Element of NAT ; :: thesis: (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n))
defpred S₁[ Element of 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: S₁[ 0 ] by A1, SIN_COS:def 22;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] by A7, A6, SIN_COS:def 22; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence (Partial_Product (JSum (Prob * A))) . n = exp_R . (- ((Partial_Sums (Prob * A)) . n)) ; :: thesis: verum