let X1, X2 be set ; :: thesis: for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
let S1 be Field_Subset of X1; :: thesis: for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
let S2 be Field_Subset of X2; :: thesis: for m1 being Measure of S1
for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
let m1 be Measure of S1; :: thesis: for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
let m2 be Measure of S2; :: thesis: for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
let E1, E2 be Element of measurable_rectangles (S1,S2); :: thesis: ( E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) implies (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2) )
assume that
A1: E1 misses E2 and
A2: E1 \/ E2 in measurable_rectangles (S1,S2) ; :: thesis: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)
set S = measurable_rectangles (S1,S2);
set P = product-pre-Measure (m1,m2);
reconsider E = E1 \/ E2 as Element of measurable_rectangles (S1,S2) by A2;
consider A being Element of S1, B being Element of S2 such that
A3: ( E = [:A,B:] & (product-pre-Measure (m1,m2)) . E = (m1 . A) * (m2 . B) ) by Def6;
consider A1 being Element of S1, B1 being Element of S2 such that
A4: ( E1 = [:A1,B1:] & (product-pre-Measure (m1,m2)) . E1 = (m1 . A1) * (m2 . B1) ) by Def6;
consider A2 being Element of S1, B2 being Element of S2 such that
A5: ( E2 = [:A2,B2:] & (product-pre-Measure (m1,m2)) . E2 = (m1 . A2) * (m2 . B2) ) by Def6;

per cases ( E1 = {} or E2 = {} or ( E1 <> {} & E2 <> {} ) ) ;

suppose ( E1 = {} or E2 = {} ) ; :: thesis: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)

then ( ( (product-pre-Measure (m1,m2)) . E1 = 0 & (product-pre-Measure (m1,m2)) . E = (product-pre-Measure (m1,m2)) . E2 ) or ( (product-pre-Measure (m1,m2)) . E2 = 0 & (product-pre-Measure (m1,m2)) . E = (product-pre-Measure (m1,m2)) . E1 ) ) by VALUED_0:def 19;
hence (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2) by XXREAL_3:4; :: thesis: verum

end;

suppose ( E1 <> {} & E2 <> {} ) ; :: thesis: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)

then A11: ( A <> {} & B <> {} & A1 <> {} & B1 <> {} & A2 <> {} & B2 <> {} ) by A3, A4, A5;

per cases ( ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) or ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ) by A1, A4, A5, A3, A11, Th23;

suppose A13: ( A1 misses A2 & A = A1 \/ A2 & B = B1 & B = B2 ) ; :: thesis: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)

then [:A1,B1:] \/ [:A2,B2:] = [:(A1 \/ A2),B:] by ZFMISC_1:97;
then (product-pre-Measure (m1,m2)) . (E1 \/ E2) = (m1 . (A1 \/ A2)) * (m2 . B) by A4, A5, Th20;
then A14: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((m1 . A1) + (m1 . A2)) * (m2 . B) by A13, MEASURE1:def 3;
( m1 . A1 >= 0 & m1 . A2 >= 0 ) by MEASURE1:def 2;
hence (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2) by A4, A5, A13, A14, XXREAL_3:96; :: thesis: verum

end;

suppose A15: ( B1 misses B2 & B = B1 \/ B2 & A = A1 & A = A2 ) ; :: thesis: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)

then [:A1,B1:] \/ [:A2,B2:] = [:A,(B1 \/ B2):] by ZFMISC_1:97;
then (product-pre-Measure (m1,m2)) . (E1 \/ E2) = (m1 . A) * (m2 . (B1 \/ B2)) by A4, A5, Th20;
then A16: (product-pre-Measure (m1,m2)) . (E1 \/ E2) = (m1 . A) * ((m2 . B1) + (m2 . B2)) by A15, MEASURE1:def 3;
( m2 . B1 >= 0 & m2 . B2 >= 0 ) by MEASURE1:def 2;
hence (product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2) by A4, A5, A15, A16, XXREAL_3:96; :: thesis: verum

end;

end;

end;

end;