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 E -measurable ;
defpred S₁[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));
A4: dom |.f.| = E by A2, MESFUNC1:def 10;

now :: thesis:

let x be object ; :: 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 EXTREAL1:15;
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.)) ;

now :: thesis:

let x be object ; :: 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, EXTREAL1:16; :: 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.)) ;
A14: |.f.| is E -measurable 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.|,(1 / (n + 1)))) ; :: thesis:
thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S₁[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) by A14, A4, MESFUNC1:27; :: thesis:

end;

consider F being sequence of S such that
A16: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(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 = 1 / (n + 1);
set En = F . n;
set g = |.f.| | (F . n);
A18: |.f.| | (F . n) is nonnegative by MESFUNC5:15;
set z = 1 / (n + 1);
A19: |.f.| | E = |.f.| by A4, RELAT_1:69;
A20: F . n = E /\ (great_eq_dom (|.f.|,(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 F . n -measurable by A14, A20, MESFUNC1:30, XBOOLE_1:17;
then A23: |.f.| | (F . n) is F . n -measurable 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, MESFUNC5:100;
then A25: Integral (M,|.f.|) < +infty by MESFUNC5:96;
A26: ((1 / (n + 1)) * (M . (F . n))) / (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;
1 / (n + 1) is R_eal by XXREAL_0:def 1;
then 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 object st x in F . n holds
nf . x = 1 / (n + 1) by MESFUNC5:41;
for x being object 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.|,(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: 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 F . n -measurable 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 / (1 / (n + 1)) = +infty by XXREAL_3:83;
integral+ (M,nf) = Integral (M,nf) by A28, A31, MESFUNC5:89;
then integral+ (M,nf) = (1 / (n + 1)) * (M . (F . n)) by A29, A30, A32, MESFUNC5:104;
then (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.|,(0 + (1 / (n + 1))))) by A16;
then E /\ (great_dom (|.f.|,0)) = union (rng F) by MESFUNC1:22;
hence ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(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: