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