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
for E being Element of S st E = dom f & f is_measurable_on E holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is_measurable_on E holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is_measurable_on E holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is_measurable_on E holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
let E be Element of S; :: thesis: ( E = dom f & f is_measurable_on E implies Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) )
assume that
A1: E = dom f and
A2: f is_measurable_on E ; :: thesis: Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
A3: ( E = dom (max+ f) & E = dom (max- f) ) by A1, MESFUNC2:def 2, MESFUNC2:def 3;
( max+ f is_measurable_on E & max- f is_measurable_on E ) by A1, A2, Th10;
then ( Integral (M,(max+ f)) = integral+ (M,(max+ f)) & Integral (M,(max- f)) = integral+ (M,(max- f)) ) by A3, Th5, MESFUNC5:88;
hence Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) by MESFUNC5:def 16; :: thesis: verum