consider IT being Measure of (Field_generated_by (measurable_rectangles (S1,S2))) such that
A1: for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
IT . E = Sum ((product-pre-Measure (M1,M2)) * F) by MEASURE9:55;
reconsider IT = IT as induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) by A1, MEASURE9:def 8;
take IT ; :: thesis: for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
IT . E = Sum ((product-pre-Measure (M1,M2)) * F)
thus for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
IT . E = Sum ((product-pre-Measure (M1,M2)) * F) by A1; :: thesis: verum