:: deftheorem Def2 defines sigmaFieldFamily MEASUR13:def 2 :
for m being Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is sigmaFieldFamily of X iff for i being Nat st i in Seg m holds
b₃ . i is SigmaField of (X . i) );