let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT ,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT ,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT ,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let f be PartFunc of X,COMPLEX ; :: thesis: ( f is_integrable_on M implies ex F being Function of NAT ,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) ) )
assume A1: f is_integrable_on M ; :: thesis: ex F being Function of NAT ,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E by Th35;
defpred S₁[ Element of NAT , set ] means $2 = E /\ (great_eq_dom |.f.|,(1 / ($1 + 1)));
A4: dom |.f.| = E by A2, VALUED_1:def 11;

now

let x be set ; :: thesis: ( x in E \ (eq_dom |.f.|,0 ) implies x in E /\ (great_dom |.f.|,0 ) )
reconsider y = |.f.| . x as Real ;
assume A5: x in E \ (eq_dom |.f.|,0 ) ; :: thesis: x in E /\ (great_dom |.f.|,0 )
then A6: x in E by XBOOLE_0:def 5;
then A7: x in dom |.f.| by A2, VALUED_1:def 11;
not x in eq_dom |.f.|,0 by A5, XBOOLE_0:def 5;
then not y = 0 by A7, MESFUNC6:7;
then not |.(f . x).| = 0 by A7, VALUED_1:def 11;
then f . x <> 0 by COMPLEX1:13, SQUARE_1:82;
then 0 < |.(f . x).| by COMPLEX1:133;
then 0 < |.f.| . x by A7, VALUED_1:def 11;
then x in great_dom |.f.|,0 by A7, MESFUNC1:def 14;
hence x in E /\ (great_dom |.f.|,0 ) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A8: E \ (eq_dom |.f.|,0 ) c= E /\ (great_dom |.f.|,0 ) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in E /\ (great_dom |.f.|,0 ) implies x in E \ (eq_dom |.f.|,0 ) )
assume A9: x in E /\ (great_dom |.f.|,0 ) ; :: thesis: x in E \ (eq_dom |.f.|,0 )
then x in great_dom |.f.|,0 by XBOOLE_0:def 4;
then 0 < |.f.| . x by MESFUNC1:def 14;
then A10: not x in eq_dom |.f.|,0 by MESFUNC1:def 16;
x in E by A9, XBOOLE_0:def 4;
hence x in E \ (eq_dom |.f.|,0 ) by A10, XBOOLE_0:def 5; :: thesis: verum

end;

then A11: E /\ (great_dom |.f.|,0 ) c= E \ (eq_dom |.f.|,0 ) by TARSKI:def 3;
A12: |.f.| is_measurable_on E by A2, A3, MESFUN6C:30;
A13: for n being Element of NAT ex Z being Element of S st S₁[n,Z]

proof

let n be Element of NAT ; :: thesis: ex Z being Element of S st S₁[n,Z]
take Z = E /\ (great_eq_dom |.f.|,(1 / (n + 1))); :: thesis: ( Z is Element of S & S₁[n,Z] )
thus ( Z is Element of S & S₁[n,Z] ) by A12, A4, MESFUNC6:13; :: thesis: verum

end;

consider F being Function of NAT ,S such that
A14: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 10(A13);
A15: for n being Nat holds
( F . n in S & M . (F . n) < +infty )

proof

|.f.| is_integrable_on M by A1, Th35;
then A16: Integral M,|.f.| < +infty by MESFUNC6:90;
let n be Nat; :: thesis: ( F . n in S & M . (F . n) < +infty )
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
set z = R_EAL (1 / (n + 1));
A17: F . n1 = E /\ (great_eq_dom |.f.|,(1 / (n1 + 1))) by A14;
then reconsider En = F . n as Element of S ;
set h = |.f.| | En;
consider nf being PartFunc of X,REAL such that
A18: nf is_simple_func_in S and
A19: dom nf = En and
A20: for x being set st x in En holds
nf . x = 1 / (n + 1) by MESFUNC6:75;
A21: dom (|.f.| | En) = En by A4, A17, RELAT_1:91, XBOOLE_1:17;
A22: F . n c= great_eq_dom |.f.|,(1 / (n + 1)) by A17, XBOOLE_1:17;
A23: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | En) . x

proof

let x be Element of X; :: thesis: ( x in dom nf implies nf . x <= (|.f.| | En) . x )
assume A24: x in dom nf ; :: thesis: nf . x <= (|.f.| | En) . x
then (|.f.| | En) . x = |.f.| . x by A19, FUNCT_1:72;
then 1 / (n + 1) <= (|.f.| | En) . x by A22, A19, A24, MESFUNC1:def 15;
hence nf . x <= (|.f.| | En) . x by A19, A20, A24; :: thesis: verum

end;

(dom |.f.|) /\ En = E /\ En by A2, VALUED_1:def 11;
then A25: (dom |.f.|) /\ En = En by A17, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is_measurable_on En by A12, A17, MESFUNC6:16, XBOOLE_1:17;
then A26: |.f.| | En is_measurable_on En by A25, MESFUNC6:76;
A27: |.f.| | En is nonnegative by Lm1, MESFUNC6:55;
for x being set st x in dom nf holds
nf . x >= 0 by A19, A20;
then A28: nf is nonnegative by MESFUNC6:52;
( |.f.| is nonnegative & |.f.| | E = |.f.| ) by A4, Lm1, RELAT_1:98;
then A29: Integral M,(|.f.| | En) <= Integral M,|.f.| by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17;
nf is_measurable_on En by A18, MESFUNC6:50;
then Integral M,nf <= Integral M,(|.f.| | En) by A21, A26, A27, A19, A28, A23, Th34;
then A30: Integral M,nf <= Integral M,|.f.| by A29, XXREAL_0:2;
A31: ( ((R_EAL (1 / (n + 1))) * (M . En)) / (R_EAL (1 / (n + 1))) = M . En & +infty / (R_EAL (1 / (n + 1))) = +infty ) by XXREAL_3:94, XXREAL_3:99;
Integral M,nf = (R_EAL (1 / (n + 1))) * (M . En) by A19, A20, MESFUNC6:97;
then (R_EAL (1 / (n + 1))) * (M . En) < +infty by A16, A30, XXREAL_0:2;
hence ( F . n in S & M . (F . n) < +infty ) by A31, XXREAL_3:91; :: thesis: verum

end;

take F ; :: thesis: ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
A32: for n being Nat holds F . n = E /\ (great_eq_dom |.f.|,(1 / (n + 1)))

proof

let n be Nat; :: thesis: F . n = E /\ (great_eq_dom |.f.|,(1 / (n + 1)))
n in NAT by ORDINAL1:def 13;
hence F . n = E /\ (great_eq_dom |.f.|,(1 / (n + 1))) by A14; :: thesis: verum

end;

then for n being Nat holds F . n = E /\ (great_eq_dom |.f.|,(0 + (1 / (n + 1)))) ;
then E /\ (great_dom |.f.|,0 ) = union (rng F) by MESFUNC6:11;
hence ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) ) & (dom f) \ (eq_dom |.f.|,0 ) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) ) by A2, A32, A11, A8, A15, XBOOLE_0:def 10; :: thesis: verum