:: deftheorem defines is_independent_wrt KOLMOG01:def 5 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for I being set
for F being ManySortedSigmaField of I,Sigma holds
( F is_independent_wrt P iff for E being finite Subset of I
for A being SigmaSection of E,F holds A is_independent_wrt P );