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 A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

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 A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_integrable_on M implies ( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M ) )

assume A1: f is_integrable_on M ; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

then Re f is_integrable_on M by MESFUN6C:def 2;

then R_EAL (Re f) is_integrable_on M by MESFUNC6:def 4;

then consider A1 being Element of S such that

A2: A1 = dom (R_EAL (Re f)) and

A3: R_EAL (Re f) is A1 -measurable ;

A4: Re f is A1 -measurable by A3, MESFUNC6:def 1;

Im f is_integrable_on M by A1, MESFUN6C:def 2;

then R_EAL (Im f) is_integrable_on M by MESFUNC6:def 4;

then consider A2 being Element of S such that

A5: A2 = dom (R_EAL (Im f)) and

A6: R_EAL (Im f) is A2 -measurable ;

A7: A1 = dom f by A2, COMSEQ_3:def 3;

A2 = dom f by A5, COMSEQ_3:def 4;

then Im f is A1 -measurable by A6, A7, MESFUNC6:def 1;

then A8: f is A1 -measurable by A4, MESFUN6C:def 1;

hence ex A being Element of S st

( A = dom f & f is A -measurable ) by A7; :: thesis: |.f.| is_integrable_on M

thus |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

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 A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_integrable_on M implies ( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M ) )

assume A1: f is_integrable_on M ; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & |.f.| is_integrable_on M )

then Re f is_integrable_on M by MESFUN6C:def 2;

then R_EAL (Re f) is_integrable_on M by MESFUNC6:def 4;

then consider A1 being Element of S such that

A2: A1 = dom (R_EAL (Re f)) and

A3: R_EAL (Re f) is A1 -measurable ;

A4: Re f is A1 -measurable by A3, MESFUNC6:def 1;

Im f is_integrable_on M by A1, MESFUN6C:def 2;

then R_EAL (Im f) is_integrable_on M by MESFUNC6:def 4;

then consider A2 being Element of S such that

A5: A2 = dom (R_EAL (Im f)) and

A6: R_EAL (Im f) is A2 -measurable ;

A7: A1 = dom f by A2, COMSEQ_3:def 3;

A2 = dom f by A5, COMSEQ_3:def 4;

then Im f is A1 -measurable by A6, A7, MESFUNC6:def 1;

then A8: f is A1 -measurable by A4, MESFUN6C:def 1;

hence ex A being Element of S st

( A = dom f & f is A -measurable ) by A7; :: thesis: |.f.| is_integrable_on M

thus |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; :: thesis: verum