Field_generated_by (measurable_rectangles (S1,S2)) = DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:22;
then A1: sigma (Field_generated_by (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2)) by Th1;
(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2))) is sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by A1, MEASURE9:61;
hence (sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2))) is induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2) by A1, MEASURE9:def 9; :: thesis: verum