let X be non empty set ; 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; 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; 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; ( 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
; ( 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; 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; verum