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 S_{1}[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));

A4: dom |.f.| = E by A2, VALUED_1:def 11;

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_{1}[n,Z]

A14: for n being Element of NAT holds S_{1}[n,F . n]
from FUNCT_2:sch 3(A13);

A15: for n being Nat holds

( F . n in S & M . (F . n) < +infty )

( F . n in S & M . (F . n) < +infty ) ) )

A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(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

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 S

A4: dom |.f.| = E by A2, VALUED_1:def 11;

now :: thesis: for x being object st x in E \ (eq_dom (|.f.|,0)) holds

x in E /\ (great_dom (|.f.|,0))

then A8:
E \ (eq_dom (|.f.|,0)) c= E /\ (great_dom (|.f.|,0))
;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 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: verum

end;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 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: verum

now :: thesis: for x being object st x in E /\ (great_dom (|.f.|,0)) holds

x in E \ (eq_dom (|.f.|,0))

then A11:
E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0))
;x in E \ (eq_dom (|.f.|,0))

let x be object ; :: thesis: ( x in E /\ (great_dom (|.f.|,0)) implies x in E \ (eq_dom (|.f.|,0)) )

assume A9: x in E /\ (great_dom (|.f.|,0)) ; :: thesis: x in E \ (eq_dom (|.f.|,0))

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: verum

end;assume A9: x in E /\ (great_dom (|.f.|,0)) ; :: thesis: x in E \ (eq_dom (|.f.|,0))

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: verum

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

proof

consider F being sequence of S such that
let n be Element of NAT ; :: thesis: ex Z being Element of S st S_{1}[n,Z]

take E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; :: thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S_{1}[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )

thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S_{1}[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
by A12, A4, MESFUNC6:13; :: thesis: verum

end;take E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; :: thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S

thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S

A14: for n being Element of NAT holds S

A15: for n being Nat holds

( F . n in S & M . (F . n) < +infty )

proof

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.| is_integrable_on M
by A1, Th35;

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 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

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: verum

end;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 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

proof

(dom |.f.|) /\ En = E /\ En
by A2, VALUED_1:def 11;
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 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: verum

end;assume A24: x in dom nf ; :: thesis: nf . x <= (|.f.| | En) . x

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: verum

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: verum

( 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

then
for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1)))))
;
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;n in NAT by ORDINAL1:def 12;

hence F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) by A14; :: thesis: verum

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