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 A -measurable ) & ( 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 A -measurable ) & ( 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 A -measurable ) & ( 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 A -measurable ) & ( 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 A -measurable ) 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 object st x in dom f holds
0 <= f . x by A2;
A4: dom (0 (#) f) = dom f by MESFUNC1:def 6;

now :: thesis: for x being object st x in dom (0 (#) f) holds
(0 (#) f) . x = f . x

let x be object ; :: 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 = 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:2
.= 0 * (integral+ (M,f)) by A1, A3, Th86, SUPINF_2:52
.= 0 ;
:: thesis: verum