:: deftheorem defines MeasureFamily MEASUR10:def 4 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being FieldFamily of X
for b₄ being b₁ -element FinSequence holds
( b₄ is MeasureFamily of S iff for i being Nat st i in Seg n holds
ex F being Field_Subset of (X . i) st
( F = S . i & b₄ . i is Measure of F ) );