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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative & c <= 0 implies Integral (M,(c (#) f)) = c * (integral' (M,f)) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: c <= 0 ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))

set d = - c;

A4: - f is_simple_func_in S by A1, Th30;

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

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

then Integral (M,(c (#) f)) = (- (- c)) * (integral' (M,(- (- f)))) by A3, A2, A4, Lm3;

hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by DBLSEQ_3:2; :: 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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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 nonnegative & c <= 0 holds

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

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative & c <= 0 implies Integral (M,(c (#) f)) = c * (integral' (M,f)) )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative and

A3: c <= 0 ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))

set d = - c;

A4: - f is_simple_func_in S by A1, Th30;

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

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

then Integral (M,(c (#) f)) = (- (- c)) * (integral' (M,(- (- f)))) by A3, A2, A4, Lm3;

hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by DBLSEQ_3:2; :: thesis: verum