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 & 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; :: 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 & 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ;

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

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 & 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; :: 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 & 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ;

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

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