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

now :: thesis: for A being object st A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } holds
lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } implies lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } ) ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } by A2;
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( W = E & Integral (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol (((A2 . n) /\ V),M2))) = (product_sigma_Measure (M1,M2)) . ((A2 . n) /\ V)

proof

let n be Nat; :: thesis: Integral (M1,(Y-vol (((A2 . n) /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) ) ;
hence Integral (M1,(Y-vol (((A2 . n) /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 = Y-vol (((A2 . $1) /\ V),M2);
T1: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]
reconsider f1 = Y-vol (((A2 . n) /\ V),M2) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f1 ; :: thesis: S₁[n,f1]
thus f1 = Y-vol (((A2 . n) /\ V),M2) ; :: thesis: verum

end;

consider F being Function of NAT,(PFuncs (X1,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 X1,ExtREAL ;
T2a: for n being Nat holds F . n = Y-vol (((A2 . n) /\ V),M2)

proof

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

end;

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

proof

let n be Nat; :: thesis: for x being Element of X1 holds (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . x
let x be Element of X1; :: thesis: (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . x
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . 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 = Y-vol (((A2 . n) /\ V),M2) & F . m = Y-vol (((A2 . m) /\ V),M2) ) by T2a;
then ( dom (F . n) = XX1 & dom (F . m) = XX1 ) by FUNCT_2:def 1;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;

T6: for n being Nat holds F . n is XX1 -measurable

proof

let n be Nat; :: thesis: F . n is XX1 -measurable
F . n = Y-vol (((A2 . n) /\ V),M2) by T2a;
hence F . n is XX1 -measurable by A01, DefYvol; :: thesis: verum

end;

T7: for n, m being Nat st n <= m holds
for x being Element of X1 st x in XX1 holds
(F . n) . x <= (F . m) . x

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X1 st x in XX1 holds
(F . n) . x <= (F . m) . x )
assume T71: n <= m ; :: thesis: for x being Element of X1 st x in XX1 holds
(F . n) . x <= (F . m) . x

hereby :: thesis: verum

let x be Element of X1; :: thesis: ( x in XX1 implies (F . n) . x <= (F . m) . x )
assume x in XX1 ; :: 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: M2 . (Measurable-X-section (((A2 . n) /\ V),x)) = (Y-vol (((A2 . n) /\ V),M2)) . x by A01, DefYvol
.= (F # x) . n by T4
.= (F . n) . x by MESFUNC5:def 13 ;
M2 . (Measurable-X-section (((A2 . m) /\ V),x)) = (Y-vol (((A2 . m) /\ V),M2)) . x by A01, DefYvol
.= (F # x) . m by T4
.= (F . m) . x by MESFUNC5:def 13 ;
hence (F . n) . x <= (F . m) . x by T72, T73, Th14, MEASURE1:31; :: thesis: verum

end;

end;

T8: for x being Element of X1 st x in XX1 holds
F # x is convergent

proof

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

proof

let x be Element of X1; :: thesis: ( x in dom (lim F) implies (lim F) . x = (Y-vol ((E /\ V),M2)) . x )
assume x in dom (lim F) ; :: thesis: (lim F) . x = (Y-vol ((E /\ V),M2)) . x
then L2: (lim F) . x = lim (F # x) by MESFUNC8:def 9;
consider G being SetSequence of S2 such that
L3: ( G is non-descending & ( for n being Nat holds G . n = (Measurable-X-section ((A2 . n),x)) /\ (Measurable-X-section (V,x)) ) & lim G = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) ) by A3, Th108;
for n being Element of NAT holds (F # x) . n = (M2 * G) . n

proof

let n be Element of NAT ; :: thesis: (F # x) . n = (M2 * G) . n
L5: dom G = NAT by FUNCT_2:def 1;
L4: (F # x) . n = (F . n) . x by MESFUNC5:def 13
.= (Y-vol (((A2 . n) /\ V),M2)) . x by T2
.= M2 . (Measurable-X-section (((A2 . n) /\ V),x)) by A01, DefYvol ;
Measurable-X-section (((A2 . n) /\ V),x) = (Measurable-X-section ((A2 . n),x)) /\ (Measurable-X-section (V,x)) by Th21;
then Measurable-X-section (((A2 . n) /\ V),x) = G . n by L3;
hence (F # x) . n = (M2 * G) . n by L4, L5, FUNCT_1:13; :: thesis: verum

end;

then F # x = M2 * G by FUNCT_2:63;
then (lim F) . x = M2 . ((Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x))) by L2, L3, MEASURE8:26;
then (lim F) . x = M2 . (Measurable-X-section ((E /\ V),x)) by Th21;
hence (lim F) . x = (Y-vol ((E /\ V),M2)) . x by A01, DefYvol; :: thesis: verum

end;

then V3: lim F = Y-vol ((E /\ V),M2) 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 (M1,(F . n)) by V2
.= Integral (M1,(Y-vol (((A2 . n) /\ V),M2))) 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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (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 = Y-vol (((A2 . $1) /\ V),M2);
T1: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]

proof

let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X1,ExtREAL) st S₁[n,f]
reconsider f1 = Y-vol (((A2 . n) /\ V),M2) as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f1 ; :: thesis: S₁[n,f1]
thus f1 = Y-vol (((A2 . n) /\ V),M2) ; :: thesis: verum

end;

consider F being Function of NAT,(PFuncs (X1,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 X1,ExtREAL ;
T2a: for n being Nat holds F . n = Y-vol (((A2 . n) /\ V),M2)

proof

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

end;

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

proof

let n be Nat; :: thesis: for x being Element of X1 holds (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . x
let x be Element of X1; :: thesis: (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . x
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n = (Y-vol (((A2 . n) /\ V),M2)) . 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 = Y-vol (((A2 . n) /\ V),M2) & F . m = Y-vol (((A2 . m) /\ V),M2) ) by T2a;
then ( dom (F . n) = XX1 & dom (F . m) = XX1 ) 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 X1,ExtREAL by MESFUNC8:def 2;
T6: for n being Nat holds
( F . n is nonnegative & F . n is XX1 -measurable )

proof

let n be Nat; :: thesis: ( F . n is nonnegative & F . n is XX1 -measurable )
F . n = Y-vol (((A2 . n) /\ V),M2) by T2a;
hence ( F . n is nonnegative & F . n is XX1 -measurable ) by A01, DefYvol; :: thesis: verum

end;

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

proof

let x be Element of X1; :: thesis: for n, m being Nat st x in XX1 & n <= m holds
(F . n) . x >= (F . m) . x
let n, m be Nat; :: thesis: ( x in XX1 & n <= m implies (F . n) . x >= (F . m) . x )
assume ( x in XX1 & 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: M2 . (Measurable-X-section (((A2 . n) /\ V),x)) = (Y-vol (((A2 . n) /\ V),M2)) . x by A01, DefYvol
.= (F # x) . n by T4
.= (F . n) . x by MESFUNC5:def 13 ;
M2 . (Measurable-X-section (((A2 . m) /\ V),x)) = (Y-vol (((A2 . m) /\ V),M2)) . x by A01, DefYvol
.= (F # x) . m by T4
.= (F . m) . x by MESFUNC5:def 13 ;
hence (F . m) . x <= (F . n) . x by T72, T73, Th14, MEASURE1:31; :: thesis: verum

end;

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

proof

let x be Element of X1; :: thesis: ( x in dom (lim F) implies (lim F) . x = (Y-vol ((E /\ V),M2)) . x )
assume x in dom (lim F) ; :: thesis: (lim F) . x = (Y-vol ((E /\ V),M2)) . x
then L2: (lim F) . x = lim (F # x) by MESFUNC8:def 9;
consider G being SetSequence of S2 such that
L3: ( G is non-ascending & ( for n being Nat holds G . n = (Measurable-X-section ((A2 . n),x)) /\ (Measurable-X-section (V,x)) ) & lim G = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) ) by A3, Th110;
G . 0 = (Measurable-X-section ((A2 . 0),x)) /\ (Measurable-X-section (V,x)) by L3;
then L31: M2 . (G . 0) <= M2 . (Measurable-X-section (V,x)) by MEASURE1:31, XBOOLE_1:17;
Measurable-X-section (V,x) c= B by A02, Th16;
then M2 . (Measurable-X-section (V,x)) <= M2 . B by MEASURE1:31;
then M2 . (G . 0) <= M2 . B by L31, XXREAL_0:2;
then LL: M2 . (G . 0) < +infty by PS2, XXREAL_0:2;
for n being Element of NAT holds (F # x) . n = (M2 * G) . n

proof

let n be Element of NAT ; :: thesis: (F # x) . n = (M2 * G) . n
L5: dom G = NAT by FUNCT_2:def 1;
L4: (F # x) . n = (F . n) . x by MESFUNC5:def 13
.= (Y-vol (((A2 . n) /\ V),M2)) . x by T2
.= M2 . (Measurable-X-section (((A2 . n) /\ V),x)) by A01, DefYvol ;
Measurable-X-section (((A2 . n) /\ V),x) = (Measurable-X-section ((A2 . n),x)) /\ (Measurable-X-section (V,x)) by Th21;
then Measurable-X-section (((A2 . n) /\ V),x) = G . n by L3;
hence (F # x) . n = (M2 * G) . n by L4, L5, FUNCT_1:13; :: thesis: verum

end;

then F # x = M2 * G by FUNCT_2:63;
then (lim F) . x = M2 . ((Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x))) by L2, L3, LL, MEASURE8:31;
then (lim F) . x = M2 . (Measurable-X-section ((E /\ V),x)) by Th21;
hence (lim F) . x = (Y-vol ((E /\ V),M2)) . x by A01, DefYvol; :: thesis: verum

end;

then V3: lim F = Y-vol ((E /\ V),M2) 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 (M1,(F . n)) by V2
.= Integral (M1,(Y-vol (((A2 . n) /\ V),M2))) 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 (M1,(Y-vol ((E /\ V),M2))) = (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 (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:] by A1, PROB_3:69; :: thesis: verum