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 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 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 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 holds

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

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

assume that

A1: f is_simple_func_in S and

a2: f is nonnegative ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))

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 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 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 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 holds

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

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

assume that

A1: f is_simple_func_in S and

a2: f is nonnegative ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))

per cases
( c >= 0 or c < 0 )
;

end;

suppose A2:
c >= 0
; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))

then A3:
( c (#) f is_simple_func_in S & c (#) f is nonnegative )
by A1, a2, MESFUNC5:20, MESFUNC5:39;

integral' (M,(c (#) f)) = c * (integral' (M,f)) by A1, a2, A2, MESFUNC5:66;

hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by A3, MESFUNC5:89; :: thesis: verum

end;integral' (M,(c (#) f)) = c * (integral' (M,f)) by A1, a2, A2, MESFUNC5:66;

hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by A3, MESFUNC5:89; :: thesis: verum