let X1, X2 be non empty set ; 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; for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))
let S2 be SigmaField of X2; 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; verum