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,REAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))
let f be PartFunc of X,REAL; :: thesis: for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))
let A be Element of S; :: thesis: ( A = dom f & f is A -measurable implies Integral (M,(- f)) = - (Integral (M,f)) )
assume that
A1: A = dom f and
A2: f is A -measurable ; :: thesis: Integral (M,(- f)) = - (Integral (M,f))
dom (R_EAL f) = dom f by MESFUNC5:def 7;
then Integral (M,(- (R_EAL f))) = - (Integral (M,(R_EAL f))) by A1, A2, MESFUNC6:def 1, MESFUN11:52;
then Integral (M,(R_EAL (- f))) = - (Integral (M,(R_EAL f))) by MESFUNC6:28;
then Integral (M,(- f)) = - (Integral (M,(R_EAL f))) by MESFUNC6:def 3;
hence Integral (M,(- f)) = - (Integral (M,f)) by MESFUNC6:def 3; :: thesis: verum