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 . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement 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 st A is_all_independent_wrt Prob holds
Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . 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 . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n
let A be SetSequence of Sigma; :: thesis: for n being Nat st A is_all_independent_wrt Prob holds
Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n
let n be Nat; :: thesis: ( A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n )
assume A1: A is_all_independent_wrt Prob ; :: thesis: Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n
defpred S1[ Nat] means Prob . ((Partial_Intersection (Complement A)) . $1) = (Partial_Product (Prob * (Complement A))) . $1;
dom (Prob * (Complement A)) = NAT by FUNCT_2:def 1;
then A2: (Prob * (Complement A)) . 0 = Prob . ((Complement A) . 0) by FUNCT_1:12;
(Partial_Product (Prob * (Complement A))) . 0 = (Prob * (Complement A)) . 0 by SERIES_3:def 1;
then A4: S1[ 0 ] by A2, PROB_3:21;
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 (Complement A)) . k) /\ ((Partial_Intersection (Complement A)) . k)) /\ ((Complement A) . (k + 1)) = ((Partial_Intersection (Complement A)) . k) /\ ((A . (k + 1)) `) by PROB_1:def 2;
then (((Partial_Intersection (Complement A)) . k) /\ ((Partial_Intersection (Complement A)) . k)) /\ ((Complement A) . (k + 1)) = ((Partial_Intersection (Complement A)) . k) /\ (Omega \ (A . (k + 1))) by SUBSET_1:def 4;
then A7: (((Partial_Intersection (Complement A)) . k) /\ ((Partial_Intersection (Complement A)) . k)) /\ ((Complement A) . (k + 1)) = (((Partial_Intersection (Complement A)) . k) /\ Omega) \ (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) by XBOOLE_1:50;
A8: ((Partial_Intersection (Complement A)) . k) /\ Omega = (Partial_Intersection (Complement A)) . k by XBOOLE_1:28;
Prob . (((Partial_Intersection (Complement A)) . k) \ (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1)))) = (Prob . ((Partial_Intersection (Complement A)) . k)) - (Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1)))) by PROB_1:33, XBOOLE_1:17;
then A10: Prob . ((Partial_Intersection (Complement A)) . (k + 1)) = (Prob . ((Partial_Intersection (Complement A)) . k)) - (Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1)))) by A7, A8, PROB_3:21;
for A being SetSequence of Sigma
for k being Nat st A is_all_independent_wrt Prob holds
Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . 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 . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * A) . (k + 1))
let k be Nat; :: thesis: ( A is_all_independent_wrt Prob implies Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * A) . (k + 1)) )
assume A11: A is_all_independent_wrt Prob ; :: thesis: Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * A) . (k + 1))
set n = k + 1;
reconsider n1 = k as Element of NAT by ORDINAL1:def 12;
n1 < k + 1 by NAT_1:13;
then Prob . (((Partial_Intersection (Complement A)) . k) /\ ((Partial_Intersection (A ^\ ((k + 0) + 1))) . (((k + 1) - k) - 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Partial_Product (Prob * (A ^\ ((k + 0) + 1)))) . (((k + 1) - k) - 1)) by A11, Th6;
then A12: Prob . (((Partial_Intersection (Complement A)) . k) /\ ((A ^\ (k + 1)) . 0)) = ((Partial_Product (Prob * (Complement A))) . 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 . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * (A ^\ (k + 1))) . 0) by A12, SERIES_3:def 1;
dom (Prob * (A ^\ (k + 1))) = NAT by FUNCT_2:def 1;
then A15: Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * (Prob . (A . (k + 1))) by A13, A14, FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
hence Prob . (((Partial_Intersection (Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (Complement A))) . k) * ((Prob * A) . (k + 1)) by A15, FUNCT_1:12; :: thesis: verum
end;
then A16: Prob . ((Partial_Intersection (Complement A)) . (k + 1)) = ((Partial_Product (Prob * (Complement A))) . k) - (((Partial_Product (Prob * (Complement A))) . 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 A17, FUNCT_1:12;
dom (Prob * (Complement A)) = NAT by FUNCT_2:def 1;
then (Prob * (Complement A)) . (k + 1) = Prob . ((Complement A) . (k + 1)) by FUNCT_1:12;
then (Prob * A) . (k + 1) = 1 - ((Prob * (Complement A)) . (k + 1)) by A18, PROB_1:def 2;
then Prob . ((Partial_Intersection (Complement A)) . (k + 1)) = (((Partial_Product (Prob * (Complement A))) . k) - ((Partial_Product (Prob * (Complement A))) . k)) + (((Partial_Product (Prob * (Complement A))) . k) * ((Prob * (Complement A)) . (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 . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n ; :: thesis: verum