A1: 1 in Seg 1 ;
Prod_Measure (L-Meas 1) = (L-Meas 1) . 1 by MEASUR13:def 13;
hence Prod_Measure (L-Meas 1) = L-Meas by A1, FUNCOP_1:7; :: thesis: for E being Element of L-Field holds E in Prod_Field (L-Field 1)
thus for E being Element of L-Field holds E in Prod_Field (L-Field 1) by Th41; :: thesis: verum