let f1, f2 be induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2); :: 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
f1 . E = Sum ((product-pre-Measure (M1,M2)) * F) ) & ( 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
f2 . E = Sum ((product-pre-Measure (M1,M2)) * F) ) implies f1 = f2 )
assume 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
f1 . E = Sum ((product-pre-Measure (M1,M2)) * F) and
A2: 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
f2 . E = Sum ((product-pre-Measure (M1,M2)) * F) ; :: thesis: f1 = f2

now :: thesis: for E being Element of Field_generated_by (measurable_rectangles (S1,S2)) holds f1 . E = f2 . E

let E be Element of Field_generated_by (measurable_rectangles (S1,S2)); :: thesis: f1 . E = f2 . E
Field_generated_by (measurable_rectangles (S1,S2)) = DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:22;
then E in DisUnion (measurable_rectangles (S1,S2)) ;
then E in { A where A is Subset of [:X1,X2:] : ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st A = Union F } by SRINGS_3:def 3;
then consider A being Subset of [:X1,X2:] such that
A3: ( E = A & ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st A = Union F ) ;
consider F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) such that
A4: E = Union F by A3;
f1 . E = Sum ((product-pre-Measure (M1,M2)) * F) by A1, A4;
hence f1 . E = f2 . E by A2, A4; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum