let X1, X2 be set ; 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; 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; 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; 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; 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 ; ( 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 )
; (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;