:: deftheorem defines sigUn KOLMOG01:def 6 :
for I being set
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being Subset of I holds sigUn (F,J) = sigma (Union (F | J));