theorem Th46: :: MEASUR14:46

( Prod_Measure (L-Meas 2) = Prod_Measure (L-Meas,L-Meas) & ( for E1, E2 being Element of L-Field holds
( [:E1,E2:] in measurable_rectangles (L-Field,L-Field) & (Prod_Measure (L-Meas 2)) . [:E1,E2:] = (L-Meas . E1) * (L-Meas . E2) ) ) )