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 c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (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 c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonpositive 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 ; :: thesis: ( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

set d = - c;

A3: (- c) (#) (- f) = (- c) (#) ((- 1) (#) f) by MESFUNC2:9

.= ((- c) * (- 1)) (#) f by Th35 ;

hence Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, Th30, Th59; :: thesis: Integral (M,(c (#) f)) = - (c * (integral' (M,(- f))))

Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, A3, Th30, Th59;

hence Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) by XXREAL_3:92; :: thesis: verum

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 holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (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 c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is_simple_func_in S & f is nonpositive holds

( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonpositive 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 ; :: thesis: ( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )

set d = - c;

A3: (- c) (#) (- f) = (- c) (#) ((- 1) (#) f) by MESFUNC2:9

.= ((- c) * (- 1)) (#) f by Th35 ;

hence Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, Th30, Th59; :: thesis: Integral (M,(c (#) f)) = - (c * (integral' (M,(- f))))

Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, A3, Th30, Th59;

hence Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) by XXREAL_3:92; :: thesis: verum