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,ExtREAL st f is_integrable_on M holds
( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) ) )
assume A1: f is_integrable_on M ; :: thesis: ( f is_integrable_on COM M & Integral (M,f) = Integral ((COM M),f) )
then consider E being Element of S such that
A2: ( E = dom f & f is E -measurable ) by MESFUNC5:def 17;
A3: ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by ;
A4: ( E = dom (max+ f) & E = dom (max- f) ) by ;
reconsider E1 = E as Element of COM (S,M) by Th27;
( max+ f is E -measurable & max- f is E -measurable ) by ;
then A5: ( integral+ (M,(max+ f)) = integral+ ((COM M),(max+ f)) & integral+ (M,(max- f)) = integral+ ((COM M),(max- f)) ) by ;
f is E1 -measurable by ;
hence f is_integrable_on COM M by ; :: thesis: Integral (M,f) = Integral ((COM M),f)
Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16;
hence Integral (M,f) = Integral ((COM M),f) by ; :: thesis: verum