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 f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
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 f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let M2 be sigma_Measure of S2; :: thesis: for f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let f be non empty PartFunc of [:X1,X2:],ExtREAL; :: thesis: for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f implies ( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_simple_func_in sigma (measurable_rectangles (S1,S2)) and
A4: ( f is nonnegative or f is nonpositive ) and
A5: A = dom f ; :: thesis: ( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
A6: f is A -measurable by A3, MESFUNC2:34;
set S = sigma (measurable_rectangles (S1,S2));
set M = Prod_Measure (M1,M2);
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
consider E being non empty Finite_Sep_Sequence of sigma (measurable_rectangles (S1,S2)), a being FinSequence of ExtREAL , r being FinSequence of REAL such that
A7: ( E,a are_Re-presentation_of f & ( for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),[:X1,X2:])) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) ) by A3, Th5;
defpred S₁[ Nat] means Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | $1))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | $1)))))));
A8: S₁[ 0 ] A14: for n being Nat st S₁[n] holds
S₁[n + 1] A28: union (rng E) = dom f by A7, MESFUNC3:def 1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A14);
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (len E)))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (len E)))))))) ;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng E)))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (len E)))))))) by FINSEQ_1:58;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) by A28, FINSEQ_1:58; :: thesis: Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
defpred S₂[ Nat] means Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | $1))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | $1)))))));
A8: S₂[ 0 ] A14: for n being Nat st S₂[n] holds
S₂[n + 1] A28: union (rng E) = dom f by A7, MESFUNC3:def 1;
for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A14);
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (len E)))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (len E)))))))) ;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng E)))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (len E)))))))) by FINSEQ_1:58;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) by A28, FINSEQ_1:58; :: thesis: verum