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 P0: 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 & Im f is_integrable_on M ) by MESFUN6C:def 4;
then P1: ( R_EAL (Re f) is_integrable_on M & R_EAL (Im f) is_integrable_on M ) by MESFUNC6:def 9;
then consider A1 being Element of S such that
P2: ( A1 = dom (R_EAL (Re f)) & R_EAL (Re f) is_measurable_on A1 ) by MESFUNC5:def 17;
consider A2 being Element of S such that
P3: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is_measurable_on A2 ) by P1, MESFUNC5:def 17;
P4: ( A1 = dom f & A2 = dom f ) by P2, P3, MESFUN6C:def 1, MESFUN6C:def 2;
then ( Re f is_measurable_on A1 & Im f is_measurable_on A1 ) by P2, P3, MESFUNC6:def 6;
then P5: f is_measurable_on A1 by MESFUN6C:def 3;
hence ex A being Element of S st
( A = dom f & f is_measurable_on A ) by P4; :: thesis: |.f.| is_integrable_on M
thus |.f.| is_integrable_on M by P0, P4, P5, MESFUN6C:31; :: thesis: verum