let X be non empty set ; 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; 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; 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; 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; 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; ( 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
; 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
;
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))
;
verum end; suppose A10:
r < 0
;
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))
;
verum end; end;