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 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,ExtREAL
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,ExtREAL
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,ExtREAL; :: 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))
set g = - f;
A4: f = - (- f) by Th36;
B6: ( dom (max- f) = A & dom (max+ f) = A ) by A1, MESFUNC2:def 2, MESFUNC2:def 3;
B7: ( max- f is A -measurable & max+ f is A -measurable ) by A1, A2, Th10;
A6: dom (- f) = A by A1, MESFUNC1:def 7;
then A7: ( dom (max+ (- f)) = A & dom (max- (- f)) = A ) by MESFUNC2:def 2, MESFUNC2:def 3;
- f is A -measurable by A1, A2, MEASUR11:63;
then A9: ( max+ (- f) is A -measurable & max- (- f) is A -measurable ) by A6, Th10;
then P1: integral+ (M,(max+ (- f))) = Integral (M,(max+ (- f))) by A7, Th5, MESFUNC5:88
.= Integral (M,(max- (- (- f)))) by Th34
.= integral+ (M,(max- f)) by A4, B6, B7, Th5, MESFUNC5:88 ;
integral+ (M,(max- (- f))) = Integral (M,(max- (- f))) by A7, A9, Th5, MESFUNC5:88
.= Integral (M,(max+ (- (- f)))) by MESFUNC2:14
.= integral+ (M,(max+ f)) by A4, B6, B7, Th5, MESFUNC5:88 ;
then Integral (M,f) = (integral+ (M,(max- (- f)))) - (integral+ (M,(max+ (- f)))) by P1, MESFUNC5:def 16
.= - ((integral+ (M,(max+ (- f)))) - (integral+ (M,(max- (- f))))) by XXREAL_3:26 ;
hence Integral (M,(- f)) = - (Integral (M,f)) by MESFUNC5:def 16; :: thesis: verum