let X1, X2 be set ; :: thesis: for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
let S1 be Field_Subset of X1; :: thesis: for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
let S2 be Field_Subset of X2; :: thesis: for m1 being Measure of S1
for m2 being Measure of S2
for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
let m1 be Measure of S1; :: thesis: for m2 being Measure of S2
for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
let m2 be Measure of S2; :: thesis: for A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
let A, B be set ; :: thesis: ( A in S1 & B in S2 implies (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B) )
assume ( A in S1 & B in S2 ) ; :: thesis: (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)
then [:A,B:] in measurable_rectangles (S1,S2) ;
then consider A1 being Element of S1, B1 being Element of S2 such that
A2: ( [:A,B:] = [:A1,B1:] & (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A1) * (m2 . B1) ) by Def6;

per cases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;

suppose A3: ( A = {} or B = {} ) ; :: thesis: (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)

then [:A,B:] = {} by ZFMISC_1:90;
then A4: (product-pre-Measure (m1,m2)) . [:A,B:] = 0 by VALUED_0:def 19;
( m1 . A = 0 or m2 . B = 0 ) by A3, VALUED_0:def 19;
hence (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B) by A4; :: thesis: verum

end;

suppose ( A <> {} & B <> {} ) ; :: thesis: (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)

then ( A = A1 & B = B1 ) by A2, ZFMISC_1:110;
hence (product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B) by A2; :: thesis: verum

end;

end;