let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for r being Real st r >= 0 holds
Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A being Element of S
for r being Real st r >= 0 holds
Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
let M be sigma_Measure of S; :: thesis: for A being Element of S
for r being Real st r >= 0 holds
Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
let A be Element of S; :: thesis: for r being Real st r >= 0 holds
Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
let r be Real; :: thesis: ( r >= 0 implies Integral (M,(r (#) (chi (A,X)))) = r * (M . A) )
assume A1: r >= 0 ; :: thesis: Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
reconsider XX = X as Element of S by MEASURE1:7;
A2: ( dom (chi (A,X)) = XX & chi (A,X) is XX -measurable ) by FUNCT_3:def 3, MESFUNC2:29;
then A3: ( dom (r (#) (chi (A,X))) = XX & r (#) (chi (A,X)) is XX -measurable ) by MESFUNC1:def 6, MESFUNC1:37;
Integral (M,(chi (A,X))) = M . A by MESFUNC9:14;
then integral+ (M,(chi (A,X))) = M . A by A2, MESFUNC5:88;
then integral+ (M,(r (#) (chi (A,X)))) = r * (M . A) by A1, A2, MESFUNC5:86;
hence Integral (M,(r (#) (chi (A,X)))) = r * (M . A) by A1, A3, MESFUNC5:20, MESFUNC5:88; :: thesis: verum