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
( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union 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 holds
( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union 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 holds
( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n ) )
let A be SetSequence of Sigma; :: thesis: for n being Nat holds
( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n ) )
let n be Nat; :: thesis: ( ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n ) )
thus ( Complement A is_all_independent_wrt Prob implies Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ) :: thesis: ( A is_all_independent_wrt Prob implies 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n )

proof

assume A1: Complement A is_all_independent_wrt Prob ; :: thesis: Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n
( (Partial_Intersection (Complement (Complement A))) . n = (Partial_Intersection A) . n & (Partial_Product (Prob * (Complement (Complement A)))) . n = (Partial_Product (Prob * A)) . n & Prob . ((Partial_Intersection (Complement (Complement A))) . n) = (Partial_Product (Prob * (Complement (Complement A)))) . n ) by A1, Th10;
hence Prob . ((Partial_Intersection A) . n) = (Partial_Product (Prob * A)) . n ; :: thesis: verum

end;

assume A is_all_independent_wrt Prob ; :: thesis: 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n
then ( Prob . ((Partial_Intersection (Complement A)) . n) = (Partial_Product (Prob * (Complement A))) . n & Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n)) ) by Th10, Th8;
hence 1 - (Prob . ((Partial_Union A) . n)) = (Partial_Product (Prob * (Complement A))) . n ; :: thesis: verum