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 15;
then 0. < |.(f . z).| by EXTREAL2:4;
then 0. < |.f.| . z by A7, MESFUNC1:def 10;
then x in great_dom (|.f.|,0.) by A7, MESFUNC1:def 13;
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 13;
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 15;
hence contradiction by A12, EXTREAL2:5; :: 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:27;
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 E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ; :: thesis:
thus ( E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) is Element of S & S₁[n,E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))))] ) by A14, A4, MESFUNC1:27; :: 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:15;
set z = R_EAL (1 / (n + 1));
A19: |.f.| | E = |.f.| by A4, RELAT_1:69;
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:62, 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:30, XBOOLE_1:17;
then A23: |.f.| | (F . n) is_measurable_on F . n by A22, MESFUNC5:42;
then A24: integral+ (M,(|.f.| | (F . n))) = Integral (M,(|.f.| | (F . n))) by A21, MESFUNC5:15, MESFUNC5:88;
|.f.| is_integrable_on M by A1, A2, A3, MESFUNC5:100;
then A25: Integral (M,|.f.|) < +infty by MESFUNC5:96;
A26: ((R_EAL (1 / (n + 1))) * (M . (F . n))) / (R_EAL (1 / (n + 1))) = M . (F . n) by XXREAL_3:88;
F . n c= E by A20, XBOOLE_1:17;
then A27: Integral (M,(|.f.| | (F . n))) <= Integral (M,|.f.|) by A2, A3, A4, A19, MESFUNC2:27, MESFUNC5:93;
consider nf being PartFunc of X,ExtREAL such that
A28: nf is_simple_func_in S and
A29: dom nf = F . n and
A30: for x being set st x in F . n holds
nf . x = R_EAL (1 / (n + 1)) by MESFUNC5:41;
for x being set st x in dom nf holds
nf . x >= 0 by A29, A30;
then A31: nf is nonnegative by SUPINF_2:52;
then A32: Integral (M,nf) = integral' (M,nf) by A28, MESFUNC5:89;
A33: F . n c= great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))) by A20, XBOOLE_1:17;
A34: 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 A35: x in dom nf ; :: thesis:
then A36: R_EAL (1 / (n + 1)) <= |.f.| . x by A33, A29, MESFUNC1:def 14;
(|.f.| | (F . n)) . x = |.f.| . x by A21, A29, A35, FUNCT_1:47;
hence nf . x <= (|.f.| | (F . n)) . x by A29, A30, A35, A36; :: thesis:

end;

nf is_measurable_on F . n by A28, MESFUNC2:34;
then integral+ (M,nf) <= integral+ (M,(|.f.| | (F . n))) by A21, A23, A18, A29, A31, A34, MESFUNC5:85;
then A37: integral+ (M,nf) <= Integral (M,|.f.|) by A24, A27, XXREAL_0:2;
A38: +infty / (R_EAL (1 / (n + 1))) = +infty by XXREAL_3:83;
integral+ (M,nf) = Integral (M,nf) by A28, A31, MESFUNC5:89;
then integral+ (M,nf) = (R_EAL (1 / (n + 1))) * (M . (F . n)) by A29, A30, A32, MESFUNC5:104;
then (R_EAL (1 / (n + 1))) * (M . (F . n)) < +infty by A25, A37, XXREAL_0:2;
hence ( F . n in S & M . (F . n) < +infty ) by A26, A38, XXREAL_3:80; :: 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:22;
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: