theorem Th45: :: MEASUR14:45

( Prod_Measure (L-Meas 1) = L-Meas & ( for E being Element of L-Field holds E in Prod_Field (L-Field 1) ) )