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 ;
Im f is_integrable_on M by ;
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 = dom f by ;
then Im f is A1 -measurable by ;
then A8: f is A1 -measurable by ;
hence ex A being Element of S st
( A = dom f & f is A -measurable ) by A7; :: thesis:
thus |.f.| is_integrable_on M by ; :: thesis: verum