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

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