let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))
let S2 be SigmaField of X2; :: thesis: sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))
Field_generated_by (measurable_rectangles (S1,S2)) = DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:22;
hence sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2)) by SRINGS_3:23; :: thesis: verum