:: deftheorem Def7 defines futSigmaFields KOLMOG01:def 7 :
for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for b₅ being Subset-Family of (bool Omega) holds
( b₅ = futSigmaFields (F,I) iff for S being Subset-Family of Omega holds
( S in b₅ iff ex E being finite Subset of I st S = sigUn (F,(I \ E)) ) );