let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
assume A1: f is_integrable_on M ; :: thesis:
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E by MESFUNC5:def 17;
defpred S₁[ Element of NAT , set ] means $2 = E /\ (great_eq_dom |.f.|,(R_EAL (1 / ($1 + 1))));
A4: dom |.f.| = E by A2, MESFUNC1:def 10;

now

let x be set ; :: thesis:
assume A5: x in E \ (eq_dom f,0. ) ; :: thesis:
then reconsider z = x as Element of X ;
reconsider y = f . z as R_eal ;
A6: x in E by A5, XBOOLE_0:def 5;
then A7: x in dom |.f.| by A2, MESFUNC1:def 10;
not x in eq_dom f,0. by A5, XBOOLE_0:def 5;
then not y = 0. by A2, A6, MESFUNC1:def 16;
then 0. < |.(f . z).| by EXTREAL2:52;
then 0. < |.f.| . z by A7, MESFUNC1:def 10;
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:

end;

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

now

let x be set ; :: thesis:
assume A9: x in E /\ (great_dom |.f.|,0. ) ; :: thesis:
then reconsider z = x as Element of X ;
x in great_dom |.f.|,0. by A9, XBOOLE_0:def 4;
then A10: 0. < |.f.| . z by MESFUNC1:def 14;
A11: x in E by A9, XBOOLE_0:def 4;
then x in dom |.f.| by A2, MESFUNC1:def 10;
then A12: 0. < |.(f . z).| by A10, MESFUNC1:def 10;
not x in eq_dom f,0.

proof

assume x in eq_dom f,0. ; :: thesis:
then f . z = 0. by MESFUNC1:def 16;
hence contradiction by A12, EXTREAL2:53; :: thesis:

end;

hence x in E \ (eq_dom f,0. ) by A11, XBOOLE_0:def 5; :: thesis:

end;

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

proof

let n be Element of NAT ; :: thesis:
take Z = E /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))); :: thesis:
thus ( Z is Element of S & S₁[n,Z] ) by A14, A4, MESFUNC1:31; :: thesis:

end;

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

proof

let n be Element of NAT ; :: thesis:
set d = R_EAL (1 / (n + 1));
set En = F . n;
set g = |.f.| | (F . n);
A18: |.f.| | (F . n) is nonnegative by MESFUNC5:21;
set z = R_EAL (1 / (n + 1));
A19: |.f.| | E = |.f.| by A4, RELAT_1:98;
A20: F . n = E /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) by A16;
then A21: dom (|.f.| | (F . n)) = F . n by A4, RELAT_1:91, XBOOLE_1:17;
(dom |.f.|) /\ (F . n) = E /\ (F . n) by A2, MESFUNC1:def 10;
then A22: (dom |.f.|) /\ (F . n) = F . n by A20, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is_measurable_on F . n by A14, A20, MESFUNC1:34, XBOOLE_1:17;
then A23: |.f.| | (F . n) is_measurable_on F . n by A22, MESFUNC5:48;
then A24: integral+ M,(|.f.| | (F . n)) = Integral M,(|.f.| | (F . n)) by A21, MESFUNC5:21, MESFUNC5:94;
|.f.| is_integrable_on M by A1, A2, A3, MESFUNC5:106;
then A25: Integral M,|.f.| < +infty by MESFUNC5:102;
A27: ((R_EAL (1 / (n + 1))) * (M . (F . n))) / (R_EAL (1 / (n + 1))) = M . (F . n) by XXREAL_3:99;
F . n c= E by A20, XBOOLE_1:17;
then A28: Integral M,(|.f.| | (F . n)) <= Integral M,|.f.| by A2, A3, A4, A19, MESFUNC2:29, MESFUNC5:99;
consider nf being PartFunc of X,ExtREAL such that
A29: nf is_simple_func_in S and
A30: dom nf = F . n and
A31: for x being set st x in F . n holds
nf . x = R_EAL (1 / (n + 1)) by MESFUNC5:47;
for x being set st x in dom nf holds
nf . x >= 0 by A30, A31;
then A32: nf is nonnegative by SUPINF_2:71;
then A33: Integral M,nf = integral' M,nf by A29, MESFUNC5:95;
A34: F . n c= great_eq_dom |.f.|,(R_EAL (1 / (n + 1))) by A20, XBOOLE_1:17;
A35: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | (F . n)) . x

proof

let x be Element of X; :: thesis:
assume A36: x in dom nf ; :: thesis:
then A37: R_EAL (1 / (n + 1)) <= |.f.| . x by A34, A30, MESFUNC1:def 15;
(|.f.| | (F . n)) . x = |.f.| . x by A21, A30, A36, FUNCT_1:70;
hence nf . x <= (|.f.| | (F . n)) . x by A30, A31, A36, A37; :: thesis:

end;

nf is_measurable_on F . n by A29, MESFUNC2:37;
then integral+ M,nf <= integral+ M,(|.f.| | (F . n)) by A21, A23, A18, A30, A32, A35, MESFUNC5:91;
then A38: integral+ M,nf <= Integral M,|.f.| by A24, A28, XXREAL_0:2;
A39: +infty / (R_EAL (1 / (n + 1))) = +infty by XXREAL_3:94;
integral+ M,nf = Integral M,nf by A29, A32, MESFUNC5:95;
then integral+ M,nf = (R_EAL (1 / (n + 1))) * (M . (F . n)) by A30, A31, A33, MESFUNC5:110;
then (R_EAL (1 / (n + 1))) * (M . (F . n)) < +infty by A25, A38, XXREAL_0:2;
hence ( F . n in S & M . (F . n) < +infty ) by A27, A39, XXREAL_3:91; :: thesis:

end;

take F ; :: thesis:
for n being Element of NAT holds F . n = E /\ (great_eq_dom |.f.|,(R_EAL (0 + (1 / (n + 1))))) by A16;
then E /\ (great_dom |.f.|,(R_EAL 0 )) = union (rng F) by MESFUNC1:26;
hence ( ( for n being Element of 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 Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) ) by A2, A16, A13, A8, A17, XBOOLE_0:def 10; :: thesis: