let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for B being Element of S2 st M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for B being Element of S2 st M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
let S2 be SigmaField of X2; :: thesis: for M2 being sigma_Measure of S2
for B being Element of S2 st M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
let M2 be sigma_Measure of S2; :: thesis: for B being Element of S2 st M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
let B be Element of S2; :: thesis: ( M2 . B < +infty implies { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:] )
assume A0: M2 . B < +infty ; :: thesis: { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
set Z = { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } ;
now :: thesis: for A being object st A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } holds
A in bool [:X1,X2:]
let A be object ; :: thesis: ( A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } implies A in bool [:X1,X2:] )
assume A in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } ; :: thesis: A in bool [:X1,X2:]
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( A = E & ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) ) ;
hence A in bool [:X1,X2:] ; :: thesis: verum
end;
then A1: { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } 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)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } holds
lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
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)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } implies lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } )
assume A2: ( A1 is monotone & rng A1 c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } ) ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
A4: for V being set st V in rng A1 holds
V in sigma (measurable_rectangles (S1,S2))
proof
let V be set ; :: thesis: ( V in rng A1 implies V in sigma (measurable_rectangles (S1,S2)) )
assume V in rng A1 ; :: thesis: V in sigma (measurable_rectangles (S1,S2))
then V in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } by A2;
then ex E being Element of sigma (measurable_rectangles (S1,S2)) st
( V = E & ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) ) ;
hence V in sigma (measurable_rectangles (S1,S2)) ; :: thesis: verum
end;
A5: 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;
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)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
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;
ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) )
proof
defpred S1[ Nat, object ] means ex f1 being Function of X1,ExtREAL st
( $2 = f1 & ( for x being Element of X1 holds
( f1 . x = M2 . ((Measurable-X-section ((A2 . $1),x)) /\ B) & ( for V being Element of S1 holds f1 is V -measurable ) ) ) );
A6: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S1[n,f]
proof
let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X1,ExtREAL) st S1[n,f]
dom A1 = NAT by FUNCT_2:def 1;
then A1 . n in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } by A2, FUNCT_1:3;
then ex E1 being Element of sigma (measurable_rectangles (S1,S2)) st
( A1 . n = E1 & ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E1,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) ) ;
then consider f1 being Function of X1,ExtREAL such that
A7: ( ( for x being Element of X1 holds f1 . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) ) & ( for V being Element of S1 holds f1 is V -measurable ) ) ;
reconsider f = f1 as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f ; :: thesis: S1[n,f]
thus S1[n,f] by A7; :: thesis: verum
end;
consider f being Function of NAT,(PFuncs (X1,ExtREAL)) such that
A8: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch 3(A6);
 A9: for n being Nat holds
( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) )
proof
let n be Nat; :: thesis: ( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) )
n is Element of NAT by ORDINAL1:def 12;
then ex f1 being Function of X1,ExtREAL st
( f . n = f1 & ( for x being Element of X1 holds
( f1 . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f1 is V -measurable ) ) ) ) by A8;
hence ( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) ) ; :: 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 is Function of X1,ExtREAL & f . m is Function of X1,ExtREAL ) by A9;
then ( dom (f . n) = X1 & dom (f . m) = X1 ) 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;
reconsider XX1 = X1 as Element of S1 by MEASURE1:11;
f . 0 is Function of X1,ExtREAL by A9;
then A10: dom (f . 0) = XX1 by FUNCT_2:def 1;
A11: for n being Nat holds f . n is XX1 -measurable by A9;
A12: for x being Element of X1 st x in X1 holds
f # x is convergent
proof
let x be Element of X1; :: thesis: ( x in X1 implies f # x is convergent )
assume x in X1 ; :: thesis: f # x is convergent
for n, m being Nat st m <= n holds
(f # x) . m <= (f # x) . n
proof
let n, m be Nat; :: thesis: ( m <= n implies (f # x) . m <= (f # x) . n )
assume Y1: m <= n ; :: thesis: (f # x) . m <= (f # x) . n
( (f # x) . m = (f . m) . x & (f # x) . n = (f . n) . x ) by MESFUNC5:def 13;
then A13: ( (f # x) . m = M2 . ((Measurable-X-section ((A2 . m),x)) /\ B) & (f # x) . n = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) ) by A9;
Measurable-X-section ((A2 . m),x) c= Measurable-X-section ((A2 . n),x) by A3, Y1, PROB_1:def 5, Th14;
hence (f # x) . m <= (f # x) . n by A13, XBOOLE_1:26, MEASURE1:31; :: thesis: verum
end;
then f # x is non-decreasing by RINFSUP2:7;
hence f # x is convergent by RINFSUP2:37; :: thesis: verum
end;
A14: dom (lim f) = X1 by A10, MESFUNC8:def 9;
then reconsider F = lim f as Function of X1,ExtREAL by FUNCT_2:def 1;
take F ; :: thesis: ( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) )
thus for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) :: thesis: for V being Element of S1 holds F is V -measurable
proof
let x be Element of X1; :: thesis: F . x = M2 . ((Measurable-X-section (E,x)) /\ B)
A15: F . x = lim (f # x) by A14, MESFUNC8:def 9;
consider G being SetSequence of X2 such that
A16: ( G is non-descending & ( for n being Nat holds G . n = X-section ((A1 . n),x) ) ) by A3, Th37;
for n being Nat holds G . n in S2
proof
let n be Nat; :: thesis: G . n in S2
A1 . n in sigma (measurable_rectangles (S1,S2)) by A5;
then X-section ((A1 . n),x) in S2 by Th44;
hence G . n in S2 by A16; :: thesis: verum
end;
then reconsider G = G as Set_Sequence of S2 by MEASURE8:def 2;
set K = B (/\) G;
A17: ( G is convergent & lim G = Union G ) by A16, SETLIM_1:63;
union (rng G) = X-section ((union (rng A2)),x) by A16, Th24;
then Union G = X-section ((union (rng A2)),x) by CARD_3:def 4
.= X-section ((Union A2),x) by CARD_3:def 4
.= Measurable-X-section (E,x) by A3, SETLIM_1:63 ;
then A18: lim (B (/\) G) = (Measurable-X-section (E,x)) /\ B by A17, SETLIM_2:92;
A19: dom (B (/\) G) = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
(B (/\) G) . n in S2
proof
let n be object ; :: thesis: ( n in NAT implies (B (/\) G) . n in S2 )
assume n in NAT ; :: thesis: (B (/\) G) . n in S2
then reconsider n1 = n as Element of NAT ;
(B (/\) G) . n1 = (G . n1) /\ B by SETLIM_2:def 5;
then (B (/\) G) . n1 = (Measurable-X-section ((A2 . n1),x)) /\ B by A16;
hence (B (/\) G) . n in S2 ; :: thesis: verum
end;
then reconsider K2 = B (/\) G as SetSequence of S2 by A19, FUNCT_2:3;
K2 is non-descending by A16, SETLIM_2:22;
then A20: lim (M2 * K2) = M2 . ((Measurable-X-section (E,x)) /\ B) by A18, MEASURE8:26;
for n being Element of NAT holds (f # x) . n = (M2 * K2) . n
proof
let n be Element of NAT ; :: thesis: (f # x) . n = (M2 * K2) . n
(f # x) . n = (f . n) . x by MESFUNC5:def 13;
then A21: (f # x) . n = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) by A9;
K2 . n = (G . n) /\ B by SETLIM_2:def 5;
then K2 . n = (Measurable-X-section ((A2 . n),x)) /\ B by A16;
hence (f # x) . n = (M2 * K2) . n by A19, A21, FUNCT_1:13; :: thesis: verum
end;
hence F . x = M2 . ((Measurable-X-section (E,x)) /\ B) by A15, A20, FUNCT_2:63; :: thesis: verum
end;
thus for V being Element of S1 holds F is V -measurable by A10, A11, A12, MESFUNC8:25, MESFUNC1:30; :: thesis: verum
end;
hence lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } ; :: thesis: verum
end;
suppose A22: A1 is non-ascending ; :: thesis: lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
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 A22, SETLIM_1:64;
defpred S1[ Nat, object ] means ex f1 being Function of X1,ExtREAL st
( $2 = f1 & ( for x being Element of X1 holds
( f1 . x = M2 . ((Measurable-X-section ((A2 . $1),x)) /\ B) & ( for V being Element of S1 holds f1 is V -measurable ) ) ) );
A23: for n being Element of NAT ex f being Element of PFuncs (X1,ExtREAL) st S1[n,f]
proof
let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X1,ExtREAL) st S1[n,f]
dom A1 = NAT by FUNCT_2:def 1;
then A1 . n in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } by A2, FUNCT_1:3;
then ex E1 being Element of sigma (measurable_rectangles (S1,S2)) st
( A1 . n = E1 & ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E1,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) ) ;
then consider f1 being Function of X1,ExtREAL such that
A24: ( ( for x being Element of X1 holds f1 . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) ) & ( for V being Element of S1 holds f1 is V -measurable ) ) ;
reconsider f = f1 as Element of PFuncs (X1,ExtREAL) by PARTFUN1:45;
take f ; :: thesis: S1[n,f]
thus S1[n,f] by A24; :: thesis: verum
end;
consider f being Function of NAT,(PFuncs (X1,ExtREAL)) such that
A25: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch 3(A23);
A26: for n being Nat holds
( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) )
proof
let n be Nat; :: thesis: ( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) )
n is Element of NAT by ORDINAL1:def 12;
then ex f1 being Function of X1,ExtREAL st
( f . n = f1 & ( for x being Element of X1 holds
( f1 . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f1 is V -measurable ) ) ) ) by A25;
hence ( f . n is Function of X1,ExtREAL & ( for x being Element of X1 holds
( (f . n) . x = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) & ( for V being Element of S1 holds f . n is V -measurable ) ) ) ) ; :: 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 is Function of X1,ExtREAL & f . m is Function of X1,ExtREAL ) by A26;
then ( dom (f . n) = X1 & dom (f . m) = X1 ) 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;
reconsider XX1 = X1 as Element of S1 by MEASURE1:11;
f . 0 is Function of X1,ExtREAL by A26;
then A27: dom (f . 0) = XX1 by FUNCT_2:def 1;
A28: for n being Nat holds f . n is XX1 -measurable by A26;
A29: for x being Element of X1 st x in X1 holds
f # x is convergent
proof
let x be Element of X1; :: thesis: ( x in X1 implies f # x is convergent )
assume x in X1 ; :: thesis: f # x is convergent
for n, m being Nat st m <= n holds
(f # x) . n <= (f # x) . m
proof
let n, m be Nat; :: thesis: ( m <= n implies (f # x) . n <= (f # x) . m )
assume Y1: m <= n ; :: thesis: (f # x) . n <= (f # x) . m
( (f # x) . m = (f . m) . x & (f # x) . n = (f . n) . x ) by MESFUNC5:def 13;
then A30: ( (f # x) . m = M2 . ((Measurable-X-section ((A2 . m),x)) /\ B) & (f # x) . n = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) ) by A26;
Measurable-X-section ((A2 . n),x) c= Measurable-X-section ((A2 . m),x) by Th14, A22, Y1, PROB_1:def 4;
hence (f # x) . n <= (f # x) . m by A30, MEASURE1:31, XBOOLE_1:26; :: thesis: verum
end;
then f # x is non-increasing by RINFSUP2:7;
hence f # x is convergent by RINFSUP2:36; :: thesis: verum
end;
A31: dom (lim f) = X1 by A27, MESFUNC8:def 9;
then reconsider F = lim f as Function of X1,ExtREAL by FUNCT_2:def 1;
A32: for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B)
proof
let x be Element of X1; :: thesis: F . x = M2 . ((Measurable-X-section (E,x)) /\ B)
lim (f # x) = M2 . ((Measurable-X-section (E,x)) /\ B)
proof
consider G being SetSequence of X2 such that
A33: ( G is non-ascending & ( for n being Nat holds G . n = X-section ((A1 . n),x) ) ) by A22, Th39;
for n being Nat holds G . n in S2
proof
let n be Nat; :: thesis: G . n in S2
A1 . n in sigma (measurable_rectangles (S1,S2)) by A5;
then X-section ((A1 . n),x) in S2 by Th44;
hence G . n in S2 by A33; :: thesis: verum
end;
then reconsider G = G as Set_Sequence of S2 by MEASURE8:def 2;
set K = B (/\) G;
A34: ( G is convergent & lim G = Intersection G ) by A33, SETLIM_1:64;
meet (rng G) = X-section ((meet (rng A2)),x) by A33, Th25;
then Intersection G = X-section ((meet (rng A2)),x) by SETLIM_1:8
.= X-section ((Intersection A2),x) by SETLIM_1:8
.= Measurable-X-section (E,x) by A22, SETLIM_1:64 ;
then A35: lim (B (/\) G) = (Measurable-X-section (E,x)) /\ B by A34, SETLIM_2:92;
(B (/\) G) . 0 = (G . 0) /\ B by SETLIM_2:def 5;
then (B (/\) G) . 0 = (Measurable-X-section ((A2 . 0),x)) /\ B by A33;
then M2 . ((B (/\) G) . 0) <= M2 . B by XBOOLE_1:17, MEASURE1:31;
then A36: M2 . ((B (/\) G) . 0) < +infty by A0, XXREAL_0:2;
A37: dom (B (/\) G) = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
(B (/\) G) . n in S2
proof
let n be object ; :: thesis: ( n in NAT implies (B (/\) G) . n in S2 )
assume n in NAT ; :: thesis: (B (/\) G) . n in S2
then reconsider n1 = n as Element of NAT ;
(B (/\) G) . n1 = (G . n1) /\ B by SETLIM_2:def 5;
then (B (/\) G) . n1 = (Measurable-X-section ((A2 . n1),x)) /\ B by A33;
hence (B (/\) G) . n in S2 ; :: thesis: verum
end;
then reconsider K2 = B (/\) G as SetSequence of S2 by A37, FUNCT_2:3;
K2 is non-ascending by A33, SETLIM_2:21;
then A38: lim (M2 * K2) = M2 . ((Measurable-X-section (E,x)) /\ B) by A35, A36, MEASURE8:31;
for n being Element of NAT holds (f # x) . n = (M2 * K2) . n
proof
let n be Element of NAT ; :: thesis: (f # x) . n = (M2 * K2) . n
(f # x) . n = (f . n) . x by MESFUNC5:def 13;
then A39: (f # x) . n = M2 . ((Measurable-X-section ((A2 . n),x)) /\ B) by A26;
K2 . n = (G . n) /\ B by SETLIM_2:def 5;
then K2 . n = (Measurable-X-section ((A2 . n),x)) /\ B by A33;
hence (f # x) . n = (M2 * K2) . n by A37, A39, FUNCT_1:13; :: thesis: verum
end;
hence lim (f # x) = M2 . ((Measurable-X-section (E,x)) /\ B) by A38, FUNCT_2:63; :: thesis: verum
end;
hence F . x = M2 . ((Measurable-X-section (E,x)) /\ B) by A31, MESFUNC8:def 9; :: thesis: verum
end;
for V being Element of S1 holds F is V -measurable by A27, A28, A29, MESFUNC8:25, MESFUNC1:30;
hence lim A1 in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } by A32; :: thesis: verum
end;
end;
end;
hence { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:] by A1, PROB_3:69; :: thesis: verum