let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let r be Real; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable implies Integral (M,(r (#) f)) = r * (Integral (M,f)) )
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E -measurable ; :: thesis: Integral (M,(r (#) f)) = r * (Integral (M,f))
A7: dom (r (#) f) = E by A1, MESFUNC1:def 6;
A8: r (#) f is E -measurable by A1, A3, MESFUNC1:37;

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

suppose A9: r >= 0 ; :: thesis: Integral (M,(r (#) f)) = r * (Integral (M,f))

Integral (M,(r (#) f)) = integral+ (M,(r (#) f)) by A2, A7, A8, A9, MESFUNC5:20, MESFUNC5:88
.= r * (integral+ (M,f)) by A1, A3, A9, A2, MESFUNC5:86
.= r * (Integral (M,f)) by A1, A3, A2, MESFUNC5:88 ;
hence Integral (M,(r (#) f)) = r * (Integral (M,f)) ; :: thesis: verum

end;

suppose A10: r < 0 ; :: thesis: Integral (M,(r (#) f)) = r * (Integral (M,f))

set r2 = - r;
r = (- 1) * (- r) ;
then r (#) f = (- 1) (#) ((- r) (#) f) by MESFUN11:35;
then A11: r (#) f = - ((- r) (#) f) by MESFUNC2:9;
A12: r (#) f is nonpositive by A2, A10, MESFUNC5:20;
Integral (M,(r (#) f)) = - (integral+ (M,(- (r (#) f)))) by A12, A7, A8, MESFUN11:57
.= - (integral+ (M,((- r) (#) f))) by A11, MESFUN11:36
.= - ((- r) * (integral+ (M,f))) by A1, A3, A10, A2, MESFUNC5:86
.= (- (- r)) * (integral+ (M,f)) by XXREAL_3:92
.= r * (Integral (M,f)) by A1, A3, A2, MESFUNC5:88 ;
hence Integral (M,(r (#) f)) = r * (Integral (M,f)) ; :: thesis: verum

end;

end;