:: deftheorem Def2 defines ManySortedSigmaField KOLMOG01:def 2 :
for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for b₄ being Function of I,(bool Sigma) holds
( b₄ is ManySortedSigmaField of I,Sigma iff for i being set st i in I holds
b₄ . i is SigmaField of Omega );