:: deftheorem Def8 defines sigmaMeasureFamily MEASUR13:def 8 :
for m being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for b₄ being b₁ -element FinSequence holds
( b₄ is sigmaMeasureFamily of S iff for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & b₄ . i is sigma_Measure of Si ) );