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

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