:: deftheorem Def3 defines FieldFamily MEASUR10:def 3 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is FieldFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is Field_Subset of (X . i) );