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_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (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 holds
( ( Complement A is_all_independent_wrt Prob implies Prob . () = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . 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_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n ) )

let A be SetSequence of Sigma; :: thesis: for n being Nat holds
( ( Complement A is_all_independent_wrt Prob implies Prob . () = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n ) )

let n be Nat; :: thesis: ( ( Complement A is_all_independent_wrt Prob implies Prob . () = (Partial_Product (Prob * A)) . n ) & ( A is_all_independent_wrt Prob implies 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n ) )
thus ( Complement A is_all_independent_wrt Prob implies Prob . () = (Partial_Product (Prob * A)) . n ) :: thesis: ( A is_all_independent_wrt Prob implies 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n )
proof
assume A1: Complement A is_all_independent_wrt Prob ; :: thesis: Prob . () = (Partial_Product (Prob * A)) . n
( (Partial_Intersection ()) . n = . n & (Partial_Product (Prob * ())) . n = (Partial_Product (Prob * A)) . n & Prob . (() . n) = (Partial_Product (Prob * ())) . n ) by ;
hence Prob . () = (Partial_Product (Prob * A)) . n ; :: thesis: verum
end;
assume A is_all_independent_wrt Prob ; :: thesis: 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n
then ( Prob . ( . n) = (Partial_Product (Prob * ())) . n & Prob . ( . n) = 1 - (Prob . (() . n)) ) by ;
hence 1 - (Prob . (() . n)) = (Partial_Product (Prob * ())) . n ; :: thesis: verum