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 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 Element of 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 Element of 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 Element of NAT st A is_all_independent_wrt Prob holds
Prob . ((@Partial_Intersection (@Complement A)) . n) = (Partial_Product (Prob * (@Complement A))) . n
let n be Element of 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 S₁[ Element of 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:22;
A3: (Partial_Product (Prob * (@Complement A))) . 0 = (Prob * (@Complement A)) . 0 by SERIES_3:def 1;
A4: S₁[ 0 ] by PROB_3:25, A2, A3;
A5: 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 A6: S₁[k] ; :: thesis: S₁[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 4;
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 5;
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;
A9: 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 XBOOLE_1:17, PROB_1:69;
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:25, A9;
for A being SetSequence of Sigma
for k being Element of 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 Element of 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 Element of 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))
consider n being Element of NAT such that
A12: n = k + 1 ;
consider n1 being Element of NAT such that
A13: n1 = k ;
n1 < k + 1 by NAT_1:13, A13;
then Prob . (((@Partial_Intersection (@Complement A)) . k) /\ ((@Partial_Intersection (@Shift_Seq (A,((k + 0) + 1)))) . ((n - k) - 1))) = ((Partial_Product (Prob * (@Complement A))) . k) * ((Partial_Product (Prob * (@Shift_Seq (A,((k + 0) + 1))))) . ((n - k) - 1)) by A12, A11, Th6, A13;
then A14: Prob . (((@Partial_Intersection (@Complement A)) . k) /\ ((@Shift_Seq (A,(k + 1))) . 0)) = ((Partial_Product (Prob * (@Complement A))) . k) * ((Partial_Product (Prob * (@Shift_Seq (A,(k + 1))))) . 0) by A12, PROB_3:25;
A15: (@Shift_Seq (A,(k + 1))) . 0 = A . (0 + (k + 1)) by NAT_1:def 3;
then A16: Prob . (((@Partial_Intersection (@Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (@Complement A))) . k) * ((Prob * (@Shift_Seq (A,(k + 1)))) . 0) by A14, SERIES_3:def 1;
dom (Prob * (@Shift_Seq (A,(k + 1)))) = NAT by FUNCT_2:def 1;
then A17: Prob . (((@Partial_Intersection (@Complement A)) . k) /\ (A . (k + 1))) = ((Partial_Product (Prob * (@Complement A))) . k) * (Prob . (A . (k + 1))) by FUNCT_1:22, A15, A16;
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 FUNCT_1:22, A17; :: thesis: verum

end;

then A18: 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 5;
then ( Prob . (A . (k + 1)) = Prob . (([#] Sigma) \ ((A . (k + 1)) `)) & (A . (k + 1)) ` is Event of Sigma ) by PROB_1:50;
then A19: Prob . (A . (k + 1)) = 1 - (Prob . ((A . (k + 1)) `)) by PROB_1:68;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then A20: (Prob * A) . (k + 1) = 1 - (Prob . ((A . (k + 1)) `)) by FUNCT_1:22, A19;
dom (Prob * (@Complement A)) = NAT by FUNCT_2:def 1;
then A21: (Prob * (@Complement A)) . (k + 1) = Prob . ((@Complement A) . (k + 1)) by FUNCT_1:22;
(Prob * A) . (k + 1) = 1 - ((Prob * (@Complement A)) . (k + 1)) by PROB_1:def 4, A21, A20;
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 A18;
hence S₁[k + 1] by SERIES_3:def 1; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
hence Prob . ((@Partial_Intersection (@Complement A)) . n) = (Partial_Product (Prob * (@Complement A))) . n ; :: thesis: verum