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;

.= 0 * (integral+ (M,f)) by A1, A3, Th86, SUPINF_2:52

.= 0 ;

:: thesis: verum

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

hence integral+ (M,f) =
integral+ (M,(0 (#) f))
by A4, FUNCT_1:2
(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;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

.= 0 * (integral+ (M,f)) by A1, A3, Th86, SUPINF_2:52

.= 0 ;

:: thesis: verum