:: deftheorem defines XL-Field MEASUR14:def 11 :
for n being non zero Nat holds XL-Field n = XProd_Field (L-Field n);