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 & f is_measurable_on E ) by MESFUNC5:def 17;
A3: |.f.| is_measurable_on E by A2, MESFUNC2:29;
A4: dom |.f.| = E by A2, MESFUNC1:def 10;
defpred S₁[ Element of NAT , set ] means $2 = E /\ (great_eq_dom |.f.|,(R_EAL (1 / ($1 + 1))));
A5: for n being Element of NAT ex Z being Element of S st S₁[n,Z]

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 A3, A4, MESFUNC1:31; :: thesis:

end;

consider F being Function of NAT ,S such that
A6: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 10(A5);
take F ; :: thesis:
for n being Element of NAT holds F . n = E /\ (great_eq_dom |.f.|,(R_EAL (0 + (1 / (n + 1))))) by A6;
then A7: E /\ (great_dom |.f.|,(R_EAL 0 )) = union (rng F) by MESFUNC1:26;

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

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

end;

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

end;

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

let x be set ; :: thesis:
assume A13: x in E \ (eq_dom f,0. ) ; :: thesis:
then A14: ( x in E & not x in eq_dom f,0. ) by XBOOLE_0:def 5;
reconsider z = x as Element of X by A13;
reconsider y = f . z as R_eal ;
not y = 0. by A2, A14, MESFUNC1:def 16;
then A15: 0. < |.(f . z).| by EXTREAL2:52;
A16: x in dom |.f.| by A2, A14, MESFUNC1:def 10;
then 0. < |.f.| . z by A15, MESFUNC1:def 10;
then x in great_dom |.f.|,0. by A16, MESFUNC1:def 14;
hence x in E /\ (great_dom |.f.|,0. ) by A14, XBOOLE_0:def 4; :: thesis:

end;

then A17: E \ (eq_dom f,0. ) c= E /\ (great_dom |.f.|,0. ) by TARSKI:def 3;
for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty )

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 . n = E /\ (great_eq_dom |.f.|,(R_EAL (1 / (n + 1)))) by A6;
then A19: ( F . n c= E & F . n c= great_eq_dom |.f.|,(R_EAL (1 / (n + 1))) ) by XBOOLE_1:17;
A20: dom (|.f.| | (F . n)) = F . n by A4, A18, RELAT_1:91, XBOOLE_1:17;
A21: |.f.| is_measurable_on F . n by A3, A18, MESFUNC1:34, XBOOLE_1:17;
(dom |.f.|) /\ (F . n) = E /\ (F . n) by A2, MESFUNC1:def 10;
then (dom |.f.|) /\ (F . n) = F . n by A18, XBOOLE_1:17, XBOOLE_1:28;
then A22: |.f.| | (F . n) is_measurable_on F . n by A21, MESFUNC5:48;
A23: |.f.| | (F . n) is nonnegative by MESFUNC5:21;
consider nf being PartFunc of X,ExtREAL such that
A24: ( nf is_simple_func_in S & dom nf = F . n & ( 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 A24;
then A25: nf is nonnegative by SUPINF_2:71;
A26: nf is_measurable_on F . n by A24, MESFUNC2:37;
for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | (F . n)) . x

let x be Element of X; :: thesis:
assume A27: x in dom nf ; :: thesis:
then A28: (|.f.| | (F . n)) . x = |.f.| . x by A20, A24, FUNCT_1:70;
R_EAL (1 / (n + 1)) <= |.f.| . x by A19, A24, A27, MESFUNC1:def 15;
hence nf . x <= (|.f.| | (F . n)) . x by A24, A27, A28; :: thesis:

end;

then A29: integral+ M,nf <= integral+ M,(|.f.| | (F . n)) by A20, A22, A23, A24, A25, A26, MESFUNC5:91;
A30: ( integral+ M,(|.f.| | (F . n)) = Integral M,(|.f.| | (F . n)) & integral+ M,nf = Integral M,nf & Integral M,nf = integral' M,nf ) by A20, A22, A23, A24, A25, MESFUNC5:94, MESFUNC5:95;
then A31: integral+ M,nf = (R_EAL (1 / (n + 1))) * (M . (F . n)) by A24, MESFUNC5:110;
|.f.| is_integrable_on M by A1, A2, MESFUNC5:106;
then A32: Integral M,|.f.| < +infty by MESFUNC5:102;
|.f.| | E = |.f.| by A4, RELAT_1:98;
then Integral M,(|.f.| | (F . n)) <= Integral M,|.f.| by A2, A4, A19, MESFUNC2:29, MESFUNC5:99;
then integral+ M,nf <= Integral M,|.f.| by A29, A30, XXREAL_0:2;
then A33: (R_EAL (1 / (n + 1))) * (M . (F . n)) < +infty by A31, A32, XXREAL_0:2;
set z = R_EAL (1 / (n + 1));
R_EAL (1 / (n + 1)) < +infty by XXREAL_0:9;
then ( ((R_EAL (1 / (n + 1))) * (M . (F . n))) / (R_EAL (1 / (n + 1))) = M . (F . n) & +infty / (R_EAL (1 / (n + 1))) = +infty ) by XXREAL_3:94, XXREAL_3:99;
hence ( F . n in S & M . (F . n) < +infty ) by A33, XXREAL_3:91; :: thesis:

end;

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, A6, A7, A12, A17, XBOOLE_0:def 10; :: thesis: