theorem Th15: :: KOLMOG01:15
for Omega, I being non empty set
for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma holds tailSigmaField (F,I) is SigmaField of Omega