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_sigma_Measure (M1,M2) is sigma_Measure of (sigma (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_sigma_Measure (M1,M2) is sigma_Measure of (sigma (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_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2 holds product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))
let M2 be sigma_Measure of S2; :: thesis: product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))
Field_generated_by (measurable_rectangles (S1,S2)) = DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:22;
then sigma (Field_generated_by (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2)) by Th1;
hence product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2))) ; :: thesis: verum