theorem Th20: :: MEASUR10:22

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 A, B being set st A in S1 & B in S2 holds
(product-pre-Measure (m1,m2)) . [:A,B:] = (m1 . A) * (m2 . B)