theorem :: MEASUR14:47

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