let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
set S = measurable_rectangles (S1,S2);
set P = product-pre-Measure (M1,M2);
let F be disjoint_valued FinSequence of measurable_rectangles (S1,S2); :: thesis:
assume A1: Union F in measurable_rectangles (S1,S2) ; :: thesis:
defpred S₁[ object , object ] means ( ( $1 in dom F implies $2 = F . $1 ) & ( not $1 in dom F implies $2 = {} ) );
A2: for n being Element of NAT ex y being Element of measurable_rectangles (S1,S2) st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:

per cases ;

suppose A3: n in dom F ; :: thesis:

then F . n in rng F by FUNCT_1:3;
hence ex y being Element of measurable_rectangles (S1,S2) st S₁[n,y] by A3; :: thesis:

end;

suppose A4: not n in dom F ; :: thesis:

{} in measurable_rectangles (S1,S2) by SETFAM_1:def 8;
hence ex y being Element of measurable_rectangles (S1,S2) st S₁[n,y] by A4; :: thesis:

end;

end;

end;

consider G being Function of NAT,(measurable_rectangles (S1,S2)) such that
A5: for n being Element of NAT holds S₁[n,G . n] from FUNCT_2:sch 3(A2);
A6: for x being object st not x in dom F holds
G . x = {}

proof

let x be object ; :: thesis:
assume A7: not x in dom F ; :: thesis:

per cases ;

suppose x in dom G ; :: thesis:

hence G . x = {} by A5, A7; :: thesis:

end;

suppose not x in dom G ; :: thesis:

hence G . x = {} by FUNCT_1:def 2; :: thesis:

end;

end;

end;

for x, y being object st x <> y holds
G . x misses G . y

proof

let x, y be object ; :: thesis:
assume A7: x <> y ; :: thesis:

per cases ;

suppose ( x in dom F & y in dom F ) ; :: thesis:

then ( G . x = F . x & G . y = F . y ) by A5;
hence G . x misses G . y by A7, PROB_2:def 2; :: thesis:

end;

suppose ( not x in dom F or not y in dom F ) ; :: thesis:

then ( G . x = {} or G . y = {} ) by A6;
hence G . x misses G . y ; :: thesis:

end;

end;

end;

then reconsider G = G as disjoint_valued Function of NAT,(measurable_rectangles (S1,S2)) by PROB_2:def 2;

now :: thesis:

let y be object ; :: thesis:
assume B1: y in (rng F) \/ {{}} ; :: thesis:

per cases by B1, XBOOLE_0:def 3;

suppose y in rng F ; :: thesis:

then consider x being object such that
A8: ( x in dom F & y = F . x ) by FUNCT_1:def 3;
y = G . x by A8, A5;
hence y in rng G by A8, FUNCT_2:4; :: thesis:

end;

suppose y in {{}} ; :: thesis:

then B3: y = {} by TARSKI:def 1;
not 0 in dom F by FINSEQ_3:24;
then G . 0 = {} by A5;
hence y in rng G by B3, FUNCT_2:4; :: thesis:

end;

end;

end;

then A10: (rng F) \/ {{}} c= rng G ;

now :: thesis:

let y be object ; :: thesis:
assume y in rng G ; :: thesis:
then consider x being Element of NAT such that
A11: y = G . x by FUNCT_2:113;

per cases ;

suppose A12: x in dom F ; :: thesis:

then y = F . x by A5, A11;
then y in rng F by A12, FUNCT_1:3;
hence y in (rng F) \/ {{}} by XBOOLE_0:def 3; :: thesis:

end;

suppose not x in dom F ; :: thesis:

then y = {} by A5, A11;
then y in {{}} by TARSKI:def 1;
hence y in (rng F) \/ {{}} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then rng G c= (rng F) \/ {{}} ;
then (rng F) \/ {{}} = rng G by A10;
then (union (rng F)) \/ (union {{}}) = union (rng G) by ZFMISC_1:78;
then (union (rng F)) \/ {} = union (rng G) by ZFMISC_1:25;
then Union F = union (rng G) by CARD_3:def 4;
then Union F = Union G by CARD_3:def 4;
then P2: (product-pre-Measure (M1,M2)) . (Union F) = SUM ((product-pre-Measure (M1,M2)) * G) by A1, Th35;
P3: (product-pre-Measure (M1,M2)) * F is nonnegative FinSequence of ExtREAL by MEASURE9:47;
P4: for n being object st n in dom ((product-pre-Measure (M1,M2)) * F) holds
((product-pre-Measure (M1,M2)) * F) . n = ((product-pre-Measure (M1,M2)) * G) . n

proof

let n be object ; :: thesis:
assume Q1: n in dom ((product-pre-Measure (M1,M2)) * F) ; :: thesis:
Q5: dom G = NAT by FUNCT_2:def 1;
F . n = G . n by A5, Q1, FUNCT_1:11;
then ((product-pre-Measure (M1,M2)) * F) . n = (product-pre-Measure (M1,M2)) . (G . n) by Q1, FUNCT_1:12;
hence ((product-pre-Measure (M1,M2)) * F) . n = ((product-pre-Measure (M1,M2)) * G) . n by Q5, Q1, FUNCT_1:13; :: thesis:

end;

for n being Element of NAT st not n in dom ((product-pre-Measure (M1,M2)) * F) holds
((product-pre-Measure (M1,M2)) * G) . n = 0

proof

let n be Element of NAT ; :: thesis:
assume L1: not n in dom ((product-pre-Measure (M1,M2)) * F) ; :: thesis:
L2: dom (product-pre-Measure (M1,M2)) = measurable_rectangles (S1,S2) by FUNCT_2:def 1;
n in NAT ;
then L4: n in dom G by FUNCT_2:def 1;

now :: thesis:

assume not F . n in dom (product-pre-Measure (M1,M2)) ; :: thesis:
then not F . n in rng F by L2;
hence not n in dom F by FUNCT_1:3; :: thesis:

end;

then G . n = {} by A5, L1, FUNCT_1:11;
then ((product-pre-Measure (M1,M2)) * G) . n = (product-pre-Measure (M1,M2)) . {} by L4, FUNCT_1:13;
hence ((product-pre-Measure (M1,M2)) * G) . n = 0 by VALUED_0:def 19; :: thesis:

end;

hence (product-pre-Measure (M1,M2)) . (Union F) = Sum ((product-pre-Measure (M1,M2)) * F) by P2, P3, P4, Th37; :: thesis: