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 E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
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 E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite & M2 is sigma_finite implies Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite ; :: thesis: Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
consider A being Set_Sequence of S1 such that
A3: ( A is non-descending & ( for n being Nat holds M1 . (A . n) < +infty ) & lim A = X1 ) by A1, LM0902a;
consider B being Set_Sequence of S2 such that
A4: ( B is non-descending & ( for n being Nat holds M2 . (B . n) < +infty ) & lim B = X2 ) by A2, LM0902a;
deffunc H₁( Element of NAT ) -> Element of bool [:X1,X2:] = [:(A . $1),(B . $1):];
consider C being Function of NAT,(bool [:X1,X2:]) such that
A5: for n being Element of NAT holds C . n = H₁(n) from FUNCT_2:sch 4();
A6: for n being Nat holds C . n = [:(A . n),(B . n):]

proof

let n be Nat; :: thesis: C . n = [:(A . n),(B . n):]
n is Element of NAT by ORDINAL1:def 12;
hence C . n = [:(A . n),(B . n):] by A5; :: thesis: verum

end;

for n being Nat holds C . n in sigma (measurable_rectangles (S1,S2))

proof

let n be Nat; :: thesis: C . n in sigma (measurable_rectangles (S1,S2))
A7: C . n = [:(A . n),(B . n):] by A6;
( A . n in S1 & B . n in S2 ) by MEASURE8:def 2;
then C . n in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } by A7;
then A8: C . n in measurable_rectangles (S1,S2) by MEASUR10:def 5;
measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2)) by PROB_1:def 9;
hence C . n in sigma (measurable_rectangles (S1,S2)) by A8; :: thesis: verum

end;

then reconsider C = C as Set_Sequence of sigma (measurable_rectangles (S1,S2)) by MEASURE8:def 2;
a9: for n, m being Nat st n <= m holds
C . n c= C . m

proof

let n, m be Nat; :: thesis: ( n <= m implies C . n c= C . m )
assume n <= m ; :: thesis: C . n c= C . m
then ( A . n c= A . m & B . n c= B . m ) by A3, A4, PROB_1:def 5;
then [:(A . n),(B . n):] c= [:(A . m),(B . m):] by ZFMISC_1:96;
then C . n c= [:(A . m),(B . m):] by A6;
hence C . n c= C . m by A6; :: thesis: verum

end;

then A9: C is non-descending by PROB_1:def 5;
then a10: lim C = Union C by SETLIM_1:63;
a11: ( lim A = Union A & lim B = Union B ) by A3, A4, SETLIM_1:63;
A15: for n being Nat holds (product_sigma_Measure (M1,M2)) . (C . n) < +infty

proof

let n be Nat; :: thesis: (product_sigma_Measure (M1,M2)) . (C . n) < +infty
A12: ( A . n in S1 & B . n in S2 & C . n in sigma (measurable_rectangles (S1,S2)) ) by MEASURE8:def 2;
C . n = [:(A . n),(B . n):] by A6;
then A13: (product_sigma_Measure (M1,M2)) . (C . n) = (M1 . (A . n)) * (M2 . (B . n)) by A12, Th10;
( M1 . (A . n) <> +infty & M1 . (A . n) <> -infty & M2 . (B . n) <> +infty & M2 . (B . n) <> -infty ) by A3, A4, SUPINF_2:51;
hence (product_sigma_Measure (M1,M2)) . (C . n) < +infty by A13, XXREAL_3:69, XXREAL_0:4; :: thesis: verum

end;

set C1 = E (/\) C;
A16: dom (E (/\) C) = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
(E (/\) C) . n in sigma (measurable_rectangles (S1,S2))

proof

let n be object ; :: thesis: ( n in NAT implies (E (/\) C) . n in sigma (measurable_rectangles (S1,S2)) )
assume n in NAT ; :: thesis: (E (/\) C) . n in sigma (measurable_rectangles (S1,S2))
then reconsider n1 = n as Element of NAT ;
(E (/\) C) . n = (C . n1) /\ E by SETLIM_2:def 5;
hence (E (/\) C) . n in sigma (measurable_rectangles (S1,S2)) ; :: thesis: verum

end;

then reconsider C1 = E (/\) C as SetSequence of sigma (measurable_rectangles (S1,S2)) by A16, FUNCT_2:3;
A17: for n being Nat holds Integral (M2,(X-vol ((E /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ (C . n))

proof

let n be Nat; :: thesis: Integral (M2,(X-vol ((E /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ (C . n))
A18: ( A . n in S1 & B . n in S2 & C . n in sigma (measurable_rectangles (S1,S2)) ) by MEASURE8:def 2;
A19: C . n = [:(A . n),(B . n):] by A6;
A20: (product_sigma_Measure (M1,M2)) . (C . n) < +infty by A15;
M1 . (A . n) < +infty by A3;
then sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ (C . n)) } by A1, A18, A19, A20, Th115;
then E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ (C . n)) } ;
then ex E1 being Element of sigma (measurable_rectangles (S1,S2)) st
( E = E1 & Integral (M2,(X-vol ((E1 /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E1 /\ (C . n)) ) ;
hence Integral (M2,(X-vol ((E /\ (C . n)),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ (C . n)) ; :: thesis: verum

end;

defpred S₁[ Element of NAT , object ] means $2 = X-vol ((E /\ (C . $1)),M1);
A21: for n being Element of NAT ex f being Element of PFuncs (X2,ExtREAL) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X2,ExtREAL) st S₁[n,f]
reconsider f1 = X-vol ((E /\ (C . n)),M1) as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take f1 ; :: thesis: S₁[n,f1]
thus f1 = X-vol ((E /\ (C . n)),M1) ; :: thesis: verum

end;

consider F being Function of NAT,(PFuncs (X2,ExtREAL)) such that
A22: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A21);
reconsider F = F as Functional_Sequence of X2,ExtREAL ;
A23: for n being Nat holds F . n = X-vol ((E /\ (C . n)),M1)

proof

let n be Nat; :: thesis: F . n = X-vol ((E /\ (C . n)),M1)
n is Element of NAT by ORDINAL1:def 12;
hence F . n = X-vol ((E /\ (C . n)),M1) by A22; :: thesis: verum

end;

reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider X12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
F . 0 = X-vol ((E /\ (C . 0)),M1) by A22;
then A24: ( dom (F . 0) = XX2 & F . 0 is nonnegative ) by FUNCT_2:def 1;
A25: for n being Nat
for x being Element of X2 holds (F # x) . n = (X-vol ((E /\ (C . n)),M1)) . x

proof

let n be Nat; :: thesis: for x being Element of X2 holds (F # x) . n = (X-vol ((E /\ (C . n)),M1)) . x
let x be Element of X2; :: thesis: (F # x) . n = (X-vol ((E /\ (C . n)),M1)) . x
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n = (X-vol ((E /\ (C . n)),M1)) . x by A23; :: thesis: verum

end;

a26: for n, m being Nat holds dom (F . n) = dom (F . m)

proof

let n, m be Nat; :: thesis: dom (F . n) = dom (F . m)
( F . n = X-vol ((E /\ (C . n)),M1) & F . m = X-vol ((E /\ (C . m)),M1) ) by A23;
then ( dom (F . n) = XX2 & dom (F . m) = XX2 ) by FUNCT_2:def 1;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;

A27: for n being Nat holds F . n is XX2 -measurable

proof

let n be Nat; :: thesis: F . n is XX2 -measurable
F . n = X-vol ((E /\ (C . n)),M1) by A23;
hence F . n is XX2 -measurable by A1, DefXvol; :: thesis: verum

end;

A28: for n, m being Nat st n <= m holds
for x being Element of X2 st x in XX2 holds
(F . n) . x <= (F . m) . x

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X2 st x in XX2 holds
(F . n) . x <= (F . m) . x )
assume A29: n <= m ; :: thesis: for x being Element of X2 st x in XX2 holds
(F . n) . x <= (F . m) . x
let x be Element of X2; :: thesis: ( x in XX2 implies (F . n) . x <= (F . m) . x )
assume x in XX2 ; :: thesis: (F . n) . x <= (F . m) . x
A30: E /\ (C . n) c= E /\ (C . m) by a9, A29, XBOOLE_1:26;
A31: M1 . (Measurable-Y-section ((E /\ (C . n)),x)) = (X-vol ((E /\ (C . n)),M1)) . x by A1, DefXvol
.= (F # x) . n by A25
.= (F . n) . x by MESFUNC5:def 13 ;
M1 . (Measurable-Y-section ((E /\ (C . m)),x)) = (X-vol ((E /\ (C . m)),M1)) . x by A1, DefXvol
.= (F # x) . m by A25
.= (F . m) . x by MESFUNC5:def 13 ;
hence (F . n) . x <= (F . m) . x by A30, A31, Th15, MEASURE1:31; :: thesis: verum

end;

A32: for x being Element of X2 st x in XX2 holds
F # x is convergent

proof

let x be Element of X2; :: thesis: ( x in XX2 implies F # x is convergent )
assume x in XX2 ; :: thesis: F # x is convergent

now :: thesis: for n, m being Nat st m <= n holds
(F # x) . m <= (F # x) . n

let n, m be Nat; :: thesis: ( m <= n implies (F # x) . m <= (F # x) . n )
assume m <= n ; :: thesis: (F # x) . m <= (F # x) . n
then (F . m) . x <= (F . n) . x by A28;
then (F # x) . m <= (F . n) . x by MESFUNC5:def 13;
hence (F # x) . m <= (F # x) . n by MESFUNC5:def 13; :: thesis: verum

end;

then F # x is non-decreasing by RINFSUP2:7;
hence F # x is convergent by RINFSUP2:37; :: thesis: verum

end;

consider I being ExtREAL_sequence such that
A33: ( ( for n being Nat holds I . n = Integral (M2,(F . n)) ) & I is convergent & Integral (M2,(lim F)) = lim I ) by A24, a26, A27, A28, A32, MESFUNC8:def 2, MESFUNC9:52;
dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
then A34: dom (lim F) = dom (X-vol (E,M1)) by A24, FUNCT_2:def 1;
for x being Element of X2 st x in dom (lim F) holds
(lim F) . x = (X-vol (E,M1)) . x

proof

let x be Element of X2; :: thesis: ( x in dom (lim F) implies (lim F) . x = (X-vol (E,M1)) . x )
assume x in dom (lim F) ; :: thesis: (lim F) . x = (X-vol (E,M1)) . x
then L2: (lim F) . x = lim (F # x) by MESFUNC8:def 9;
consider G being SetSequence of S1 such that
L3: ( G is non-descending & ( for n being Nat holds G . n = (Measurable-Y-section ((C . n),x)) /\ (Measurable-Y-section (E,x)) ) & lim G = (Measurable-Y-section (X12,x)) /\ (Measurable-Y-section (E,x)) ) by A9, a11, A3, A4, a10, A6, Th116, Th109;
for n being Element of NAT holds (F # x) . n = (M1 * G) . n

proof

let n be Element of NAT ; :: thesis: (F # x) . n = (M1 * G) . n
L5: dom G = NAT by FUNCT_2:def 1;
L4: (F # x) . n = (F . n) . x by MESFUNC5:def 13
.= (X-vol (((C . n) /\ E),M1)) . x by A22
.= M1 . (Measurable-Y-section (((C . n) /\ E),x)) by A1, DefXvol ;
Measurable-Y-section (((C . n) /\ E),x) = (Measurable-Y-section ((C . n),x)) /\ (Measurable-Y-section (E,x)) by Th21;
then Measurable-Y-section (((C . n) /\ E),x) = G . n by L3;
hence (F # x) . n = (M1 * G) . n by L4, L5, FUNCT_1:13; :: thesis: verum

end;

then F # x = M1 * G by FUNCT_2:63;
then (lim F) . x = M1 . ((Measurable-Y-section (E,x)) /\ (Measurable-Y-section (X12,x))) by L2, L3, MEASURE8:26;
then (lim F) . x = M1 . (Measurable-Y-section ((E /\ X12),x)) by Th21
.= M1 . (Measurable-Y-section (E,x)) by XBOOLE_1:28 ;
hence (lim F) . x = (X-vol (E,M1)) . x by A1, DefXvol; :: thesis: verum

end;

then V3: lim F = X-vol (E,M1) by A34, PARTFUN1:5;
set J = E (/\) C;
E1: dom (E (/\) C) = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
(E (/\) C) . n in sigma (measurable_rectangles (S1,S2))

proof

let n be object ; :: thesis: ( n in NAT implies (E (/\) C) . n in sigma (measurable_rectangles (S1,S2)) )
assume n in NAT ; :: thesis: (E (/\) C) . n in sigma (measurable_rectangles (S1,S2))
then reconsider n1 = n as Element of NAT ;
(E (/\) C) . n = (C . n1) /\ E by SETLIM_2:def 5;
hence (E (/\) C) . n in sigma (measurable_rectangles (S1,S2)) ; :: thesis: verum

end;

then reconsider J = E (/\) C as SetSequence of sigma (measurable_rectangles (S1,S2)) by E1, FUNCT_2:3;
R11: J is non-descending by A9, SETLIM_2:22;
C is convergent by A9, SETLIM_1:63;
then R13: lim J = E /\ (lim C) by SETLIM_2:92
.= E /\ [:X1,X2:] by a11, A3, A4, a10, A6, Th116
.= E by XBOOLE_1:28 ;
R3: product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by Th2;
then R4: dom (product_sigma_Measure (M1,M2)) = sigma (measurable_rectangles (S1,S2)) by FUNCT_2:def 1;
rng J c= sigma (measurable_rectangles (S1,S2)) by RELAT_1:def 19;
then R2: (product_sigma_Measure (M1,M2)) /* J = (product_sigma_Measure (M1,M2)) * J by R4, FUNCT_2:def 11;
for n being Element of NAT holds I . n = ((product_sigma_Measure (M1,M2)) /* J) . n

proof

let n be Element of NAT ; :: thesis: I . n = ((product_sigma_Measure (M1,M2)) /* J) . n
R21: dom J = NAT by FUNCT_2:def 1;
I . n = Integral (M2,(F . n)) by A33
.= Integral (M2,(X-vol (((C . n) /\ E),M1))) by A22
.= (product_sigma_Measure (M1,M2)) . ((C . n) /\ E) by A17
.= (product_sigma_Measure (M1,M2)) . (J . n) by SETLIM_2:def 5 ;
hence I . n = ((product_sigma_Measure (M1,M2)) /* J) . n by R2, R21, FUNCT_1:13; :: thesis: verum

end;

then I = (product_sigma_Measure (M1,M2)) /* J by FUNCT_2:63;
hence Integral (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E by A33, V3, R13, R11, R2, R3, MEASURE8:26; :: thesis: verum