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 sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
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 sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 holds sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2 holds sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
let M2 be sigma_Measure of S2; :: thesis: sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
set C = C_Meas (product_Measure (M1,M2));
set F = Field_generated_by (measurable_rectangles (S1,S2));
Field_generated_by (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2))) by MEASURE8:20;
then sigma (Field_generated_by (measurable_rectangles (S1,S2))) c= sigma_Field (C_Meas (product_Measure (M1,M2))) by PROB_1:def 9;
then sigma (DisUnion (measurable_rectangles (S1,S2))) c= sigma_Field (C_Meas (product_Measure (M1,M2))) by SRINGS_3:22;
hence sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2))) by Th1; :: thesis: verum