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 r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
let M be sigma_Measure of S; :: thesis: for E being Element of S
for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
let E be Element of S; :: thesis: for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
let r be Real; :: thesis: Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
A3: chi (E,X) is_simple_func_in S by Th12;
Integral (M,(r (#) (chi (E,X)))) = r * (integral' (M,(chi (E,X)))) by Th12, MESFUN11:59;
hence Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X)))) by A3, MESFUNC5:89; :: thesis: verum