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
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
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
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
let M2 be sigma_Measure of S2; :: thesis: for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
let E1, E2 be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( E1 misses E2 implies (product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2) )
assume A1: E1 misses E2 ; :: thesis: (product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by Th2;
hence (product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2) by A1, MEASURE1:30; :: thesis: verum