let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( 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 ) ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( 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 ) ) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( 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 ) ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_integrable_on M implies ex F being sequence of S st
( ( 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 ) ) ) )

assume A1: f is_integrable_on M ; :: thesis: ex F being sequence of S st
( ( 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 ) ) )

then consider E being Element of S such that
A2: E = dom f and
A3: f is E -measurable by Th35;
defpred S1[ Element of NAT , set ] means \$2 = E /\ (great_eq_dom (|.f.|,(1 / (\$1 + 1))));
A4: dom |.f.| = E by ;
now :: thesis: for x being object st x in E \ (eq_dom (|.f.|,0)) holds
x in E /\ (great_dom (|.f.|,0))
let x be object ; :: thesis: ( x in E \ (eq_dom (|.f.|,0)) implies x in E /\ (great_dom (|.f.|,0)) )
reconsider y = |.f.| . x as Real ;
assume A5: x in E \ (eq_dom (|.f.|,0)) ; :: thesis: x in E /\ (great_dom (|.f.|,0))
then A6: x in E by XBOOLE_0:def 5;
then A7: x in dom |.f.| by ;
not x in eq_dom (|.f.|,0) by ;
then not y = 0 by ;
then not |.(f . x).| = 0 by ;
then f . x <> 0 by ;
then 0 < |.(f . x).| by COMPLEX1:47;
then 0 < |.f.| . x by ;
then x in great_dom (|.f.|,0) by ;
hence x in E /\ (great_dom (|.f.|,0)) by ; :: thesis: verum
end;
then A8: E \ (eq_dom (|.f.|,0)) c= E /\ (great_dom (|.f.|,0)) ;
now :: thesis: for x being object st x in E /\ (great_dom (|.f.|,0)) holds
x in E \ (eq_dom (|.f.|,0))
end;
then A11: E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0)) ;
A12: |.f.| is E -measurable by ;
A13: for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be Element of NAT ; :: thesis: ex Z being Element of S st S1[n,Z]
take E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; :: thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) by ; :: thesis: verum
end;
consider F being sequence of S such that
A14: for n being Element of NAT holds S1[n,F . n] from A15: for n being Nat holds
( F . n in S & M . (F . n) < +infty )
proof
|.f.| is_integrable_on M by ;
then A16: Integral (M,|.f.|) < +infty by MESFUNC6:90;
let n be Nat; :: thesis: ( F . n in S & M . (F . n) < +infty )
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 ;
A22: F . n c= great_eq_dom (|.f.|,(1 / (n + 1))) by ;
A23: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | En) . x
proof
let x be Element of X; :: thesis: ( x in dom nf implies nf . x <= (|.f.| | En) . x )
assume A24: x in dom nf ; :: thesis: nf . x <= (|.f.| | En) . x
then (|.f.| | En) . x = |.f.| . x by ;
then 1 / (n + 1) <= (|.f.| | En) . x by ;
hence nf . x <= (|.f.| | En) . x by ; :: thesis: verum
end;
(dom |.f.|) /\ En = E /\ En by ;
then A25: (dom |.f.|) /\ En = En by ;
|.f.| is En -measurable by ;
then A26: |.f.| | En is En -measurable by ;
A27: |.f.| | En is nonnegative by ;
for x being object st x in dom nf holds
nf . x >= 0 by ;
then A28: nf is nonnegative by MESFUNC6:52;
( |.f.| is nonnegative & |.f.| | E = |.f.| ) by ;
then A29: Integral (M,(|.f.| | En)) <= Integral (M,|.f.|) by ;
nf is En -measurable by ;
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 ;
A31: ( ((1 / (n + 1)) * (M . En)) / (1 / (n + 1)) = M . En & +infty / (1 / (n + 1)) = +infty ) by ;
Integral (M,nf) = (1 / (n + 1)) * (M . En) by ;
then (1 / (n + 1)) * (M . En) < +infty by ;
hence ( F . n in S & M . (F . n) < +infty ) by ; :: thesis: verum
end;
take F ; :: thesis: ( ( 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 ) ) )

A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
proof
let n be Nat; :: thesis: F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
n in NAT by ORDINAL1:def 12;
hence F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) by A14; :: thesis: verum
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: verum