:: deftheorem Def6 defines is_all_independent_wrt BOR_CANT:def 6 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma holds
( A is_all_independent_wrt Prob iff for B being SetSequence of Sigma st ex e being sequence of NAT st
( e is one-to-one & ( for n being Nat holds A . (e . n) = B . n ) ) holds
for n being Nat holds (Partial_Product (Prob * B)) . n = Prob . ((Partial_Intersection B) . n) );