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 E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
let M1 be sigma_Measure of S1; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite implies ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) ) )
assume M1 is sigma_finite ; :: thesis: ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
then consider B being Set_Sequence of S1 such that
A1: ( B is non-descending & ( for n being Nat holds M1 . (B . n) < +infty ) & lim B = X1 ) by LM0902a;
defpred S1[ Nat, object ] means ex f1 being Function of X2,ExtREAL st
( $2 = f1 & ( for y being Element of X2 holds
( f1 . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . $1)) & ( for V being Element of S2 holds f1 is V -measurable ) ) ) );
A2: for n being Element of NAT ex f being Element of PFuncs (X2,ExtREAL) st S1[n,f]
proof
let n be Element of NAT ; :: thesis: ex f being Element of PFuncs (X2,ExtREAL) st S1[n,f]
reconsider Bn = B . n as Element of S1 by MEASURE8:def 2;
M1 . Bn < +infty by A1;
then sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ Bn) ) & ( for V being Element of S2 holds F is V -measurable ) ) } by Th89;
then E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ Bn) ) & ( for V being Element of S2 holds F is V -measurable ) ) } ;
then ex E1 being Element of sigma (measurable_rectangles (S1,S2)) st
( E = E1 & ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E1,y)) /\ Bn) ) & ( for V being Element of S2 holds F is V -measurable ) ) ) ;
then consider f1 being Function of X2,ExtREAL such that
A3: ( ( for y being Element of X2 holds f1 . y = M1 . ((Measurable-Y-section (E,y)) /\ Bn) ) & ( for V being Element of S2 holds f1 is V -measurable ) ) ;
reconsider f = f1 as Element of PFuncs (X2,ExtREAL) by PARTFUN1:45;
take f ; :: thesis: S1[n,f]
( f1 is Function of X2,ExtREAL & f = f1 & ( for y being Element of X2 holds f1 . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) ) & ( for V being Element of S2 holds f1 is V -measurable ) ) by A3;
hence S1[n,f] ; :: thesis: verum
end;
consider f being Function of NAT,(PFuncs (X2,ExtREAL)) such that
A4: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch 3(A2);
 A5: for n being Nat holds
( f . n is Function of X2,ExtREAL & ( for y being Element of X2 holds
( (f . n) . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) & ( for V being Element of S2 holds f . n is V -measurable ) ) ) )
proof
let n be Nat; :: thesis: ( f . n is Function of X2,ExtREAL & ( for y being Element of X2 holds
( (f . n) . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) & ( for V being Element of S2 holds f . n is V -measurable ) ) ) )
n is Element of NAT by ORDINAL1:def 12;
then ex f1 being Function of X2,ExtREAL st
( f . n = f1 & ( for y being Element of X2 holds
( f1 . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) & ( for V being Element of S2 holds f1 is V -measurable ) ) ) ) by A4;
hence ( f . n is Function of X2,ExtREAL & ( for y being Element of X2 holds
( (f . n) . y = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) & ( for V being Element of S2 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 X2,ExtREAL & f . m is Function of X2,ExtREAL ) by A5;
then ( dom (f . n) = X2 & dom (f . m) = X2 ) 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;
reconsider XX2 = X2 as Element of S2 by MEASURE1:11;
f . 0 is Function of X2,ExtREAL by A5;
then A6: dom (f . 0) = XX2 by FUNCT_2:def 1;
A7: for n being Nat holds f . n is XX2 -measurable by A5;
A11: for y being Element of X2 st y in X2 holds
f # y is convergent
proof
let y be Element of X2; :: thesis: ( y in X2 implies f # y is convergent )
assume y in X2 ; :: thesis: f # y is convergent
for n, m being Nat st m <= n holds
(f # y) . m <= (f # y) . n
proof
let n, m be Nat; :: thesis: ( m <= n implies (f # y) . m <= (f # y) . n )
assume A8: m <= n ; :: thesis: (f # y) . m <= (f # y) . n
( (f # y) . m = (f . m) . y & (f # y) . n = (f . n) . y ) by MESFUNC5:def 13;
then A9: ( (f # y) . m = M1 . ((Measurable-Y-section (E,y)) /\ (B . m)) & (f # y) . n = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) ) by A5;
A10: (Measurable-Y-section (E,y)) /\ (B . m) c= (Measurable-Y-section (E,y)) /\ (B . n) by A1, A8, PROB_1:def 5, XBOOLE_1:26;
( B . m in S1 & B . n in S1 ) by MEASURE8:def 2;
then ( (Measurable-Y-section (E,y)) /\ (B . m) in S1 & (Measurable-Y-section (E,y)) /\ (B . n) in S1 ) by MEASURE1:11;
hence (f # y) . m <= (f # y) . n by A9, A10, MEASURE1:31; :: thesis: verum
end;
then f # y is non-decreasing by RINFSUP2:7;
hence f # y is convergent by RINFSUP2:37; :: thesis: verum
end;
A12: dom (lim f) = X2 by A6, MESFUNC8:def 9;
then reconsider F = lim f as Function of X2,ExtREAL by FUNCT_2:def 1;
take F ; :: thesis: ( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
thus for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) :: thesis: for V being Element of S2 holds F is V -measurable
proof
let y be Element of X2; :: thesis: F . y = M1 . (Measurable-Y-section (E,y))
deffunc H1( Nat) -> Element of bool X1 = (Measurable-Y-section (E,y)) /\ (B . $1);
set K1 = (Measurable-Y-section (E,y)) (/\) B;
B is convergent by A1, SETLIM_1:80;
then lim ((Measurable-Y-section (E,y)) (/\) B) = (Measurable-Y-section (E,y)) /\ X1 by A1, SETLIM_2:92;
then A13: lim ((Measurable-Y-section (E,y)) (/\) B) = Measurable-Y-section (E,y) by XBOOLE_1:28;
A14: dom ((Measurable-Y-section (E,y)) (/\) B) = NAT by FUNCT_2:def 1;
for n being object st n in NAT holds
((Measurable-Y-section (E,y)) (/\) B) . n in S1
proof
let n be object ; :: thesis: ( n in NAT implies ((Measurable-Y-section (E,y)) (/\) B) . n in S1 )
assume n in NAT ; :: thesis: ((Measurable-Y-section (E,y)) (/\) B) . n in S1
then reconsider n1 = n as Element of NAT ;
A15: ((Measurable-Y-section (E,y)) (/\) B) . n1 = (Y-section (E,y)) /\ (B . n1) by SETLIM_2:def 5;
reconsider Bn = B . n1 as Element of S1 by MEASURE8:def 2;
for y being Element of X2 holds (Y-section (E,y)) /\ Bn in S1
proof
let y be Element of X2; :: thesis: (Y-section (E,y)) /\ Bn in S1
Y-section (E,y) in S1 by Th44;
hence (Y-section (E,y)) /\ Bn in S1 by MEASURE1:11; :: thesis: verum
end;
hence ((Measurable-Y-section (E,y)) (/\) B) . n in S1 by A15; :: thesis: verum
end;
then reconsider K1 = (Measurable-Y-section (E,y)) (/\) B as SetSequence of S1 by A14, FUNCT_2:3;
K1 is non-descending by A1, SETLIM_2:22;
then A16: lim (M1 * K1) = M1 . (Measurable-Y-section (E,y)) by A13, MEASURE8:26;
for n being Element of NAT holds (f # y) . n = (M1 * K1) . n
proof
let n be Element of NAT ; :: thesis: (f # y) . n = (M1 * K1) . n
(f # y) . n = (f . n) . y by MESFUNC5:def 13;
then A17: (f # y) . n = M1 . ((Measurable-Y-section (E,y)) /\ (B . n)) by A5;
K1 . n = (Measurable-Y-section (E,y)) /\ (B . n) by SETLIM_2:def 5;
hence (f # y) . n = (M1 * K1) . n by A14, A17, FUNCT_1:13; :: thesis: verum
end;
then lim (f # y) = M1 . (Measurable-Y-section (E,y)) by A16, FUNCT_2:63;
hence F . y = M1 . (Measurable-Y-section (E,y)) by A12, MESFUNC8:def 9; :: thesis: verum
end;
thus for V being Element of S2 holds F is V -measurable by A11, MESFUNC1:30, A6, A7, MESFUNC8:25; :: thesis: verum