let X be non empty set ; 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; 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; 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; 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; ( 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
; 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; verum