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 E -measurable 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 E -measurable 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 E -measurable 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 E -measurable holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
let E be Element of S; :: thesis: ( E = dom f & f is E -measurable implies Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f))) )
assume that
A1: E = dom f and
A2: f is E -measurable ; :: 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 E -measurable & max- f is E -measurable ) 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