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

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let f be PartFunc of X,ExtREAL; :: thesis: for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let A, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive implies 0 >= Integral (M,(f | A)) )

assume that

A1: E = dom f and

A2: f is E -measurable and

A3: f is nonpositive ; :: thesis: 0 >= Integral (M,(f | A))

reconsider E1 = E /\ A as Element of S ;

A4: dom (f | A) = E1 by A1, RELAT_1:61;

A5: E1 = (dom f) /\ E1 by A1, XBOOLE_1:17, XBOOLE_1:28;

f is E1 -measurable by A2, XBOOLE_1:17, MESFUNC1:30;

then A6: f | E1 is E1 -measurable by A5, MESFUNC5:42;

f | E1 = (f | E) | A by RELAT_1:71;

hence 0 >= Integral (M,(f | A)) by A1, A3, A4, A6, Th61, Th1; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let f be PartFunc of X,ExtREAL; :: thesis: for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds

0 >= Integral (M,(f | A))

let A, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive implies 0 >= Integral (M,(f | A)) )

assume that

A1: E = dom f and

A2: f is E -measurable and

A3: f is nonpositive ; :: thesis: 0 >= Integral (M,(f | A))

reconsider E1 = E /\ A as Element of S ;

A4: dom (f | A) = E1 by A1, RELAT_1:61;

A5: E1 = (dom f) /\ E1 by A1, XBOOLE_1:17, XBOOLE_1:28;

f is E1 -measurable by A2, XBOOLE_1:17, MESFUNC1:30;

then A6: f | E1 is E1 -measurable by A5, MESFUNC5:42;

f | E1 = (f | E) | A by RELAT_1:71;

hence 0 >= Integral (M,(f | A)) by A1, A3, A4, A6, Th61, Th1; :: thesis: verum