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 A1, MESFUNC5:def 17;
A4: ( E = dom (max+ f) & E = dom (max- f) ) by A2, MESFUNC2:def 2, MESFUNC2:def 3;
reconsider E1 = E as Element of COM (S,M) by Th27;
( max+ f is E -measurable & max- f is E -measurable ) by A2, MESFUN11:10;
then A5: ( integral+ (M,(max+ f)) = integral+ ((COM M),(max+ f)) & integral+ (M,(max- f)) = integral+ ((COM M),(max- f)) ) by A4, Th37, MESFUN11:5;
f is E1 -measurable by A2, Th30;
hence f is_integrable_on COM M by A2, A5, A3, MESFUNC5:def 17; :: 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 A5, MESFUNC5:def 16; :: thesis: verum