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_measurable_on A ) & |.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_measurable_on A ) & |.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_measurable_on A ) & |.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_measurable_on A ) & |.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_measurable_on A ) & |.f.| is_integrable_on M )
then Re f is_integrable_on M by MESFUN6C:def 4;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def 9;
then consider A1 being Element of S such that
A2: A1 = dom (R_EAL (Re f)) and
A3: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def 17;
A4: Re f is_measurable_on A1 by A3, MESFUNC6:def 6;
Im f is_integrable_on M by A1, MESFUN6C:def 4;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def 9;
then consider A2 being Element of S such that
A5: A2 = dom (R_EAL (Im f)) and
A6: R_EAL (Im f) is_measurable_on A2 by MESFUNC5:def 17;
A7: A1 = dom f by A2, MESFUN6C:def 1;
A2 = dom f by A5, MESFUN6C:def 2;
then Im f is_measurable_on A1 by A6, A7, MESFUNC6:def 6;
then A8: f is_measurable_on A1 by A4, MESFUN6C:def 3;
hence ex A being Element of S st
( A = dom f & f is_measurable_on A ) by A7; :: thesis: |.f.| is_integrable_on M
thus |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; :: thesis: verum