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