let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 holds product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 holds product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 holds product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2 holds product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
let M2 be sigma_Measure of S2; :: thesis: product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2)
set P = measurable_rectangles (S1,S2);
set M = product-pre-Measure (M1,M2);
A2: for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st Union F in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union F) = Sum ((product-pre-Measure (M1,M2)) * F) by Th38;
for K being disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) st Union K in measurable_rectangles (S1,S2) holds
(product-pre-Measure (M1,M2)) . (Union K) <= SUM ((product-pre-Measure (M1,M2)) * K) by Th35;
hence product-pre-Measure (M1,M2) is pre-Measure of measurable_rectangles (S1,S2) by A2, MEASURE9:def 7; :: thesis: verum