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 ) & f is nonpositive holds
0 >= Integral (M,f)
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 ) & f is nonpositive holds
0 >= Integral (M,f)
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 ) & f is nonpositive holds
0 >= Integral (M,f)
let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive implies 0 >= Integral (M,f) )
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: f is nonpositive ; :: thesis: 0 >= Integral (M,f)
consider A being Element of S such that
A3: A = dom f and
a3: f is A -measurable by A1;
A4: A = dom (- f) by A3, MESFUNC1:def 7;
Integral (M,(- f)) >= 0 by A4, A2, A3, a3, MEASUR11:63, MESFUNC5:90;
then A7: integral+ (M,(- f)) >= 0 by A4, A2, A3, a3, MEASUR11:63, MESFUNC5:88;
Integral (M,f) = - (integral+ (M,(- f))) by A2, A3, a3, Th57;
hence 0 >= Integral (M,f) by A7; :: thesis: verum