:: deftheorem Def4 defines SigmaSection KOLMOG01:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for I being set
for J being Subset of I
for F being ManySortedSigmaField of I,Sigma
for b₆ being Function of J,Sigma holds
( b₆ is SigmaSection of J,F iff for i being set st i in J holds
b₆ . i in F . i );