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 st A is_all_independent_wrt Prob holds
Prob . ( . n) = (Partial_Product (Prob * ())) . n

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat st A is_all_independent_wrt Prob holds
Prob . ( . n) = (Partial_Product (Prob * ())) . n

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma
for n being Nat st A is_all_independent_wrt Prob holds
Prob . ( . n) = (Partial_Product (Prob * ())) . n

let A be SetSequence of Sigma; :: thesis: for n being Nat st A is_all_independent_wrt Prob holds
Prob . ( . n) = (Partial_Product (Prob * ())) . n

let n be Nat; :: thesis: ( A is_all_independent_wrt Prob implies Prob . ( . n) = (Partial_Product (Prob * ())) . n )
assume A1: A is_all_independent_wrt Prob ; :: thesis: Prob . ( . n) = (Partial_Product (Prob * ())) . n
defpred S1[ Nat] means Prob . ( . \$1) = (Partial_Product (Prob * ())) . \$1;
dom (Prob * ()) = NAT by FUNCT_2:def 1;
then A2: (Prob * ()) . 0 = Prob . (() . 0) by FUNCT_1:12;
A3: (Partial_Product (Prob * ())) . 0 = (Prob * ()) . 0 by SERIES_3:def 1;
A4: S1[ 0 ] by ;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
(((Partial_Intersection ()) . k) /\ ( . k)) /\ (() . (k + 1)) = ( . k) /\ ((A . (k + 1)) `) by PROB_1:def 2;
then (((Partial_Intersection ()) . k) /\ ( . k)) /\ (() . (k + 1)) = ( . k) /\ (Omega \ (A . (k + 1))) by SUBSET_1:def 4;
then A7: (((Partial_Intersection ()) . k) /\ ( . k)) /\ (() . (k + 1)) = (( . k) /\ Omega) \ (( . k) /\ (A . (k + 1))) by XBOOLE_1:50;
A8: ((Partial_Intersection ()) . k) /\ Omega = . k by XBOOLE_1:28;
A9: Prob . (( . k) \ (( . k) /\ (A . (k + 1)))) = (Prob . ( . k)) - (Prob . (( . k) /\ (A . (k + 1)))) by ;
A10: Prob . ( . (k + 1)) = (Prob . ( . k)) - (Prob . (( . k) /\ (A . (k + 1)))) by ;
for A being SetSequence of Sigma
for k being Nat st A is_all_independent_wrt Prob holds
Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1))
proof
let A be SetSequence of Sigma; :: thesis: for k being Nat st A is_all_independent_wrt Prob holds
Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1))

let k be Nat; :: thesis: ( A is_all_independent_wrt Prob implies Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1)) )
assume A11: A is_all_independent_wrt Prob ; :: thesis: Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1))
reconsider n = k + 1 as Element of NAT ;
reconsider n1 = k as Element of NAT by ORDINAL1:def 12;
n1 < k + 1 by NAT_1:13;
then Prob . (( . k) /\ ((Partial_Intersection (A ^\ ((k + 0) + 1))) . ((n - k) - 1))) = ((Partial_Product (Prob * ())) . k) * ((Partial_Product (Prob * (A ^\ ((k + 0) + 1)))) . ((n - k) - 1)) by ;
then A12: Prob . (( . k) /\ ((A ^\ (k + 1)) . 0)) = ((Partial_Product (Prob * ())) . k) * ((Partial_Product (Prob * (A ^\ (k + 1)))) . 0) by PROB_3:21;
A13: (A ^\ (k + 1)) . 0 = A . (0 + (k + 1)) by NAT_1:def 3;
then A14: Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * (A ^\ (k + 1))) . 0) by ;
dom (Prob * (A ^\ (k + 1))) = NAT by FUNCT_2:def 1;
then A15: Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * (Prob . (A . (k + 1))) by ;
dom (Prob * A) = NAT by FUNCT_2:def 1;
hence Prob . (( . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1)) by ; :: thesis: verum
end;
then A16: Prob . ( . (k + 1)) = ((Partial_Product (Prob * ())) . k) - (((Partial_Product (Prob * ())) . k) * ((Prob * A) . (k + 1))) by A6, A10, A1;
( A . (k + 1) = ((A . (k + 1)) `) ` & ((A . (k + 1)) `) ` = Omega \ ((A . (k + 1)) `) ) by SUBSET_1:def 4;
then ( Prob . (A . (k + 1)) = Prob . (([#] Sigma) \ ((A . (k + 1)) `)) & (A . (k + 1)) ` is Event of Sigma ) by PROB_1:20;
then A17: Prob . (A . (k + 1)) = 1 - (Prob . ((A . (k + 1)) `)) by PROB_1:32;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then A18: (Prob * A) . (k + 1) = 1 - (Prob . ((A . (k + 1)) `)) by ;
dom (Prob * ()) = NAT by FUNCT_2:def 1;
then A19: (Prob * ()) . (k + 1) = Prob . (() . (k + 1)) by FUNCT_1:12;
(Prob * A) . (k + 1) = 1 - ((Prob * ()) . (k + 1)) by ;
then Prob . ( . (k + 1)) = (((Partial_Product (Prob * ())) . k) - ((Partial_Product (Prob * ())) . k)) + (((Partial_Product (Prob * ())) . k) * ((Prob * ()) . (k + 1))) by A16;
hence S1[k + 1] by SERIES_3:def 1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A5);
hence Prob . ( . n) = (Partial_Product (Prob * ())) . n ; :: thesis: verum