:: deftheorem defines XL-Meas MEASUR14:def 12 :
for n being non zero Nat holds XL-Meas n = XProd_Measure (L-Meas n);