let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
let f be PartFunc of X,ExtREAL; for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
let c be Real; ( f is_simple_func_in S & f is nonpositive & 0 <= c implies ( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) ) )
assume that
A1:
f is_simple_func_in S
and
A2:
f is nonpositive
and
A3:
0 <= c
; ( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
A4:
c (#) f is_simple_func_in S
by A1, MESFUNC5:39;
f = - (max- f)
by A2, Th32;
then A6:
- f = max- f
by Th36;
A7:
- f is_simple_func_in S
by A1, Th30;
A8:
max- (c (#) f) = c (#) (max- f)
by A3, MESFUNC5:26;
c (#) f is nonpositive
by A2, A3, Th4;
hence Integral (M,(c (#) f)) =
- (integral' (M,(max- (c (#) f))))
by A4, Th58
.=
- (c * (integral' (M,(- f))))
by A3, A7, A6, A8, Th5, MESFUNC5:66
;
Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f)))
hence
Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f)))
by XXREAL_3:92; verum