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;