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,COMPLEX; :: 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 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;

let x be object ; :: thesis:
reconsider y = |.f.| . x as Real ;
assume A5: x in E \ (eq_dom (|.f.|,0)) ; :: thesis:
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:5, SQUARE_1:17;
then 0 < |.(f . x).| by COMPLEX1:47;
then 0 < |.f.| . x by A7, VALUED_1:def 11;
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)) ;

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

end;

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

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 A12, A4, MESFUNC6:13; :: thesis:

end;

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

|.f.| is_integrable_on M by A1, Th35;
then A16: Integral (M,|.f.|) < +infty by MESFUNC6:90;
let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
set z = 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 object st x in En holds
nf . x = 1 / (n + 1) by MESFUNC6:75;
A21: dom (|.f.| | En) = En by A4, A17, RELAT_1:62, 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

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

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 En -measurable by A12, A17, MESFUNC6:16, XBOOLE_1:17;
then A26: |.f.| | En is En -measurable by A25, MESFUNC6:76;
A27: |.f.| | En is nonnegative by Lm1, MESFUNC6:55;
for x being object 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;
then A29: Integral (M,(|.f.| | En)) <= Integral (M,|.f.|) by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17;
nf is En -measurable 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: ( ((1 / (n + 1)) * (M . En)) / (1 / (n + 1)) = M . En & +infty / (1 / (n + 1)) = +infty ) by XXREAL_3:83, XXREAL_3:88;
Integral (M,nf) = (1 / (n + 1)) * (M . En) by A19, A20, MESFUNC6:97;
then (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:80; :: thesis:

end;

take F ; :: thesis:
A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))

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

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.|,(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; :: thesis: