product ((Seg n) --> REAL) = REAL n by SRINGS_5:8;
hence XProd_Measure (L-Meas n) is sigma_Measure of (XL-Field n) ; :: thesis: verum