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 nonpositive & 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 nonpositive & 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 nonpositive & 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 nonpositive & 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 nonpositive & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))
let r be Real; :: thesis: ( E = dom f & f is nonpositive & f is E -measurable implies Integral (M,(r (#) f)) = r * (Integral (M,f)) )
assume that
A1: E = dom f and
A2: f is nonpositive and
A3: f is E -measurable ; :: thesis: Integral (M,(r (#) f)) = r * (Integral (M,f))
set f2 = - f;
A4: dom (- f) = E by A1, MESFUNC1:def 7;
then A5: E = dom (r (#) (- f)) by MESFUNC1:def 6;
A6: - f is E -measurable by A1, A3, MEASUR11:63;
f = - (- f) by MESFUN11:36;
then f = (- 1) (#) (- f) by MESFUNC2:9;
then r (#) f = (r * (- 1)) (#) (- f) by MESFUN11:35;
then r (#) f = (- 1) (#) (r (#) (- f)) by MESFUN11:35;
then r (#) f = - (r (#) (- f)) by MESFUNC2:9;
then Integral (M,(r (#) f)) = - (Integral (M,(r (#) (- f)))) by A5, A6, A4, MESFUNC1:37, MESFUN11:52
.= (- 1) * (Integral (M,(r (#) (- f)))) by XXREAL_3:91
.= (- 1) * (r * (Integral (M,(- f)))) by A2, A4, Lm1, A1, A3, MEASUR11:63
.= ((- 1) * r) * (Integral (M,(- f))) by XXREAL_3:66
.= (- r) * (- (Integral (M,f))) by A1, A3, MESFUN11:52
.= (- r) * ((- 1) * (Integral (M,f))) by XXREAL_3:91
.= ((- r) * (- 1)) * (Integral (M,f)) by XXREAL_3:66 ;
hence Integral (M,(r (#) f)) = r * (Integral (M,f)) ; :: thesis: verum