:: deftheorem defines XProd_Field MEASUR14:def 7 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X holds XProd_Field S = CopyField ((CarProd X),(Prod_Field S));