let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ M,f = 0
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ M,f = 0
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ M,f = 0
let f be PartFunc of X,ExtREAL ; :: thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & ( for x being Element of X st x in dom f holds
0 = f . x ) implies integral+ M,f = 0 )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: for x being Element of X st x in dom f holds
0 = f . x ; :: thesis: integral+ M,f = 0
A3: for x being set st x in dom f holds
0 <= f . x by A2;
A4: dom (0 (#) f) = dom f by MESFUNC1:def 6;

now

let x be set ; :: thesis: ( x in dom (0 (#) f) implies (0 (#) f) . x = f . x )
assume A5: x in dom (0 (#) f) ; :: thesis: (0 (#) f) . x = f . x
hence (0 (#) f) . x = (R_EAL 0 ) * (f . x) by MESFUNC1:def 6
.= 0
.= f . x by A2, A4, A5 ;
:: thesis: verum

end;

hence integral+ M,f = integral+ M,(0 (#) f) by A4, FUNCT_1:9
.= (R_EAL 0 ) * (integral+ M,f) by A1, A3, Th92, SUPINF_2:71
.= 0 ;
:: thesis: verum