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 being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative 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 being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative holds
0 <= Integral (M,(f | A))
let A be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative implies 0 <= Integral (M,(f | A)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is E -measurable ) and
A2: f is nonnegative ; :: thesis: 0 <= Integral (M,(f | A))
consider E being Element of S such that
A3: E = dom f and
A4: f is E -measurable by A1;
A5: ex C being Element of S st
( C = dom (f | A) & f | A is C -measurable )

proof

take C = E /\ A; :: thesis: ( C = dom (f | A) & f | A is C -measurable )
thus dom (f | A) = C by A3, RELAT_1:61; :: thesis: f | A is C -measurable
A6: C = (dom f) /\ C by A3, XBOOLE_1:17, XBOOLE_1:28;
A7: dom (f | A) = C by A3, RELAT_1:61
.= dom (f | C) by A6, RELAT_1:61 ;
A8: for x being object st x in dom (f | A) holds
(f | A) . x = (f | C) . x

proof

let x be object ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | C) . x )
assume A9: x in dom (f | A) ; :: thesis: (f | A) . x = (f | C) . x
then (f | A) . x = f . x by FUNCT_1:47;
hence (f | A) . x = (f | C) . x by A7, A9, FUNCT_1:47; :: thesis: verum

end;

f is C -measurable by A4, MESFUNC1:30, XBOOLE_1:17;
then f | C is C -measurable by A6, Th42;
hence f | A is C -measurable by A7, A8, FUNCT_1:2; :: thesis: verum

end;

then 0 <= integral+ (M,(f | A)) by A2, Th15, Th79;
hence 0 <= Integral (M,(f | A)) by A2, A5, Th15, Th88; :: thesis: verum