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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let M2 be sigma_Measure of S2; :: thesis: for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let V be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let A be Element of S1; :: thesis: for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
let B be Element of S2; :: thesis: ( M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty implies { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:] )
assume that
A01: M1 is sigma_finite and
A02: V = [:A,B:] and
A0: (product_sigma_Measure (M1,M2)) . V < +infty and
PS2: M1 . A < +infty ; :: thesis: { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
set Z = { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } ;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;

now :: thesis: for A being object st A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } holds
A in bool [:X1,X2:]

let A be object ; :: thesis: ( A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } implies A in bool [:X1,X2:] )
assume A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } ; :: thesis: A in bool [:X1,X2:]
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( A = E & Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) ) ;
hence A in bool [:X1,X2:] ; :: thesis: verum

end;

then A1: { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } c= bool [:X1,X2:] ;
for A1 being SetSequence of [:X1,X2:] st A1 is monotone & rng A1 c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } holds
lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

proof

let A1 be SetSequence of [:X1,X2:]; :: thesis: ( A1 is monotone & rng A1 c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } implies lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } )
assume A2: ( A1 is monotone & rng A1 c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } ) ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
A4: for V being set st V in rng A1 holds
V in sigma (measurable_rectangles (S1,S2))

proof

let W be set ; :: thesis: ( W in rng A1 implies W in sigma (measurable_rectangles (S1,S2)) )
assume W in rng A1 ; :: thesis: W in sigma (measurable_rectangles (S1,S2))
then W in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by A2;
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( W = E & Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) ) ;
hence W in sigma (measurable_rectangles (S1,S2)) ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: A1 . n in sigma (measurable_rectangles (S1,S2))
dom A1 = NAT by FUNCT_2:def 1;
then n in dom A1 by ORDINAL1:def 12;
hence A1 . n in sigma (measurable_rectangles (S1,S2)) by A4, FUNCT_1:3; :: thesis: verum

end;

then reconsider A2 = A1 as Set_Sequence of sigma (measurable_rectangles (S1,S2)) by MEASURE8:def 2;
PP: for n being Nat holds Integral (M2,(X-vol (((A2 . n) /\ V),M1))) = (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V)

proof

let n be Nat; :: thesis: Integral (M2,(X-vol (((A2 . n) /\ V),M1))) = (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V)
dom A2 = NAT by FUNCT_2:def 1;
then n in dom A2 by ORDINAL1:def 12;
then A2 . n in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by A2, FUNCT_1:3;
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( A2 . n = E & Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) ) ;
hence Integral (M2,(X-vol (((A2 . n) /\ V),M1))) = (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V) ; :: thesis: verum

end;

per cases ( A1 is non-descending or A1 is non-ascending ) by A2, SETLIM_1:def 1;

suppose A3: A1 is non-descending ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

union (rng A1) in sigma (measurable_rectangles (S1,S2)) by A4, MEASURE1:35;
then Union A1 in sigma (measurable_rectangles (S1,S2)) by CARD_3:def 4;
then reconsider E = lim A1 as Element of sigma (measurable_rectangles (S1,S2)) by A3, SETLIM_1:63;
defpred S₁[ Element of NAT , object ] means $2 = X-vol (((A2 . $1) /\ V),M1);
T1: 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 (((A2 . n) /\ V),M1) as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take f1 ; :: thesis: S₁[n,f1]
thus f1 = X-vol (((A2 . n) /\ V),M1) ; :: thesis: verum

end;

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

proof

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

end;

F . 0 = X-vol (((A2 . 0) /\ V),M1) by T2;
then T3: ( dom (F . 0) = XX2 & F . 0 is nonnegative ) by FUNCT_2:def 1;
T4: for n being Nat
for x being Element of X2 holds (F # x) . n = (X-vol (((A2 . n) /\ V),M1)) . x

proof

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

end;

T5: 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 (((A2 . n) /\ V),M1) & F . m = X-vol (((A2 . m) /\ V),M1) ) by T2a;
then ( dom (F . n) = XX2 & dom (F . m) = XX2 ) by FUNCT_2:def 1;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;

T6: 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 (((A2 . n) /\ V),M1) by T2a;
hence F . n is XX2 -measurable by A01, DefXvol; :: thesis: verum

end;

T7: 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 T71: n <= m ; :: thesis: for x being Element of X2 st x in XX2 holds
(F . n) . x <= (F . m) . x

hereby :: thesis: verum

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
T72: (A2 . n) /\ V c= (A2 . m) /\ V by A3, T71, PROB_1:def 5, XBOOLE_1:26;
T73: M1 . (Measurable-Y-section (((A2 . n) /\ V),x)) = (X-vol (((A2 . n) /\ V),M1)) . x by A01, DefXvol
.= (F # x) . n by T4
.= (F . n) . x by MESFUNC5:def 13 ;
M1 . (Measurable-Y-section (((A2 . m) /\ V),x)) = (X-vol (((A2 . m) /\ V),M1)) . x by A01, DefXvol
.= (F # x) . m by T4
.= (F . m) . x by MESFUNC5:def 13 ;
hence (F . n) . x <= (F . m) . x by T72, T73, Th15, MEASURE1:31; :: thesis: verum

end;

end;

T8: 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 T7;
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
V2: ( ( for n being Nat holds I . n = Integral (M2,(F . n)) ) & I is convergent & Integral (M2,(lim F)) = lim I ) by T3, T5, T6, T7, T8, MESFUNC9:52, MESFUNC8:def 2;
dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
then V4: dom (lim F) = dom (X-vol ((E /\ V),M1)) by T3, FUNCT_2:def 1;
for x being Element of X2 st x in dom (lim F) holds
(lim F) . x = (X-vol ((E /\ V),M1)) . x

proof

let x be Element of X2; :: thesis: ( x in dom (lim F) implies (lim F) . x = (X-vol ((E /\ V),M1)) . x )
assume x in dom (lim F) ; :: thesis: (lim F) . x = (X-vol ((E /\ V),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 ((A2 . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim G = (Measurable-Y-section (E,x)) /\ (Measurable-Y-section (V,x)) ) by A3, 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 (((A2 . n) /\ V),M1)) . x by T2
.= M1 . (Measurable-Y-section (((A2 . n) /\ V),x)) by A01, DefXvol ;
Measurable-Y-section (((A2 . n) /\ V),x) = (Measurable-Y-section ((A2 . n),x)) /\ (Measurable-Y-section (V,x)) by Th21;
then Measurable-Y-section (((A2 . n) /\ V),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 (V,x))) by L2, L3, MEASURE8:26;
then (lim F) . x = M1 . (Measurable-Y-section ((E /\ V),x)) by Th21;
hence (lim F) . x = (X-vol ((E /\ V),M1)) . x by A01, DefXvol; :: thesis: verum

end;

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

proof

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

end;

then reconsider J = V (/\) A2 as SetSequence of sigma (measurable_rectangles (S1,S2)) by E1, FUNCT_2:3;
R11: J is non-descending by A3, SETLIM_2:22;
A2 is convergent by A3, SETLIM_1:63;
then R13: lim J = E /\ V by SETLIM_2:92;
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 V2
.= Integral (M2,(X-vol (((A2 . n) /\ V),M1))) by T2
.= (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V) by PP
.= (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 lim I = lim ((product_sigma_Measure (M1,M2)) /* J) by FUNCT_2:63;
then lim I = (product_sigma_Measure (M1,M2)) . (E /\ V) by R13, R11, R2, R3, MEASURE8:26;
hence lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by V2, V3; :: thesis: verum

end;

suppose A3: A1 is non-ascending ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }

meet (rng A1) in sigma (measurable_rectangles (S1,S2)) by A4, MEASURE1:35;
then Intersection A1 in sigma (measurable_rectangles (S1,S2)) by SETLIM_1:8;
then reconsider E = lim A1 as Element of sigma (measurable_rectangles (S1,S2)) by A3, SETLIM_1:64;
defpred S₁[ Element of NAT , object ] means $2 = X-vol (((A2 . $1) /\ V),M1);
T1: 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 (((A2 . n) /\ V),M1) as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take f1 ; :: thesis: S₁[n,f1]
thus f1 = X-vol (((A2 . n) /\ V),M1) ; :: thesis: verum

end;

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

proof

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

end;

F . 0 = X-vol (((A2 . 0) /\ V),M1) by T2;
then T3: dom (F . 0) = XX2 by FUNCT_2:def 1;
T4: for n being Nat
for x being Element of X2 holds (F # x) . n = (X-vol (((A2 . n) /\ V),M1)) . x

proof

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

end;

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 (((A2 . n) /\ V),M1) & F . m = X-vol (((A2 . m) /\ V),M1) ) by T2a;
then ( dom (F . n) = XX2 & dom (F . m) = XX2 ) by FUNCT_2:def 1;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;

then reconsider F = F as with_the_same_dom Functional_Sequence of X2,ExtREAL by MESFUNC8:def 2;
T6: for n being Nat holds
( F . n is nonnegative & F . n is XX2 -measurable )

proof

let n be Nat; :: thesis: ( F . n is nonnegative & F . n is XX2 -measurable )
F . n = X-vol (((A2 . n) /\ V),M1) by T2a;
hence ( F . n is nonnegative & F . n is XX2 -measurable ) by A01, DefXvol; :: thesis: verum

end;

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

proof

let x be Element of X2; :: thesis: for n, m being Nat st x in XX2 & n <= m holds
(F . n) . x >= (F . m) . x
let n, m be Nat; :: thesis: ( x in XX2 & n <= m implies (F . n) . x >= (F . m) . x )
assume ( x in XX2 & n <= m ) ; :: thesis: (F . n) . x >= (F . m) . x
then T72: (A2 . m) /\ V c= (A2 . n) /\ V by A3, PROB_1:def 4, XBOOLE_1:26;
T73: M1 . (Measurable-Y-section (((A2 . n) /\ V),x)) = (X-vol (((A2 . n) /\ V),M1)) . x by A01, DefXvol
.= (F # x) . n by T4
.= (F . n) . x by MESFUNC5:def 13 ;
M1 . (Measurable-Y-section (((A2 . m) /\ V),x)) = (X-vol (((A2 . m) /\ V),M1)) . x by A01, DefXvol
.= (F # x) . m by T4
.= (F . m) . x by MESFUNC5:def 13 ;
hence (F . m) . x <= (F . n) . x by T72, T73, Th15, MEASURE1:31; :: thesis: verum

end;

M3: product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2))) by Th2;
Integral (M2,((F . 0) | XX2)) = Integral (M2,(X-vol (((A2 . 0) /\ V),M1))) by T2a;
then M1: Integral (M2,((F . 0) | XX2)) = (product_sigma_Measure (M1,M2)) . ((A2 . 0) /\ V) by PP;
(product_sigma_Measure (M1,M2)) . ((A2 . 0) /\ V) <= (product_sigma_Measure (M1,M2)) . V by M3, MEASURE1:31, XBOOLE_1:17;
then Integral (M2,((F . 0) | XX2)) < +infty by A0, M1, XXREAL_0:2;
then consider I being ExtREAL_sequence such that
V2: ( ( for n being Nat holds I . n = Integral (M2,(F . n)) ) & I is convergent & lim I = Integral (M2,(lim F)) ) by T3, T6, T7, MESFUN10:18;
dom (lim F) = dom (F . 0) by MESFUNC8:def 9;
then V4: dom (lim F) = dom (X-vol ((E /\ V),M1)) by T3, FUNCT_2:def 1;
for x being Element of X2 st x in dom (lim F) holds
(lim F) . x = (X-vol ((E /\ V),M1)) . x

proof

let x be Element of X2; :: thesis: ( x in dom (lim F) implies (lim F) . x = (X-vol ((E /\ V),M1)) . x )
assume x in dom (lim F) ; :: thesis: (lim F) . x = (X-vol ((E /\ V),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-ascending & ( for n being Nat holds G . n = (Measurable-Y-section ((A2 . n),x)) /\ (Measurable-Y-section (V,x)) ) & lim G = (Measurable-Y-section (E,x)) /\ (Measurable-Y-section (V,x)) ) by A3, Th111;
G . 0 = (Measurable-Y-section ((A2 . 0),x)) /\ (Measurable-Y-section (V,x)) by L3;
then L31: M1 . (G . 0) <= M1 . (Measurable-Y-section (V,x)) by MEASURE1:31, XBOOLE_1:17;
Measurable-Y-section (V,x) c= A by A02, Th16;
then M1 . (Measurable-Y-section (V,x)) <= M1 . A by MEASURE1:31;
then M1 . (G . 0) <= M1 . A by L31, XXREAL_0:2;
then LL: M1 . (G . 0) < +infty by PS2, XXREAL_0:2;
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 (((A2 . n) /\ V),M1)) . x by T2
.= M1 . (Measurable-Y-section (((A2 . n) /\ V),x)) by A01, DefXvol ;
Measurable-Y-section (((A2 . n) /\ V),x) = (Measurable-Y-section ((A2 . n),x)) /\ (Measurable-Y-section (V,x)) by Th21;
then Measurable-Y-section (((A2 . n) /\ V),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 (V,x))) by L2, L3, LL, MEASURE8:31;
then (lim F) . x = M1 . (Measurable-Y-section ((E /\ V),x)) by Th21;
hence (lim F) . x = (X-vol ((E /\ V),M1)) . x by A01, DefXvol; :: thesis: verum

end;

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

proof

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

end;

then reconsider J = V (/\) A2 as SetSequence of sigma (measurable_rectangles (S1,S2)) by E1, FUNCT_2:3;
R11: J is non-ascending by A3, SETLIM_2:21;
A2 is convergent by A3, SETLIM_1:64;
then R13: lim J = E /\ V by SETLIM_2:92;
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;
(A2 . 0) /\ V c= V by XBOOLE_1:17;
then J . 0 c= V by SETLIM_2:def 5;
then (product_sigma_Measure (M1,M2)) . (J . 0) <= (product_sigma_Measure (M1,M2)) . V by R3, MEASURE1:31;
then K1: (product_sigma_Measure (M1,M2)) . (J . 0) < +infty by A0, XXREAL_0:2;
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 V2
.= Integral (M2,(X-vol (((A2 . n) /\ V),M1))) by T2
.= (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V) by PP
.= (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 lim I = lim ((product_sigma_Measure (M1,M2)) /* J) by FUNCT_2:63;
then lim I = (product_sigma_Measure (M1,M2)) . (E /\ V) by R13, R11, R2, R3, K1, MEASURE8:31;
hence lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by V2, V3; :: thesis: verum

end;

end;

end;

hence { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:] by A1, PROB_3:69; :: thesis: verum