:: deftheorem Def6 defines product-pre-Measure MEASUR10:def 6 :
for X1, X2 being 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 b₇ being zeroed nonnegative Function of (measurable_rectangles (S1,S2)),ExtREAL holds
( b₇ = product-pre-Measure (m1,m2) iff for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b₇ . C = (m1 . A) * (m2 . B) ) );