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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & 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_measurable_on E ) & f is nonnegative implies 0 <= integral+ M,(f | A) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) 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_measurable_on E by A1;
set C = E /\ A;
A5: E /\ A = dom (f | A) by A3, RELAT_1:90;
A6: dom (f | A) = E /\ A by A3, RELAT_1:90
.= (dom f) /\ (E /\ A) by A3, XBOOLE_1:17, XBOOLE_1:28
.= dom (f | (E /\ A)) by RELAT_1:90 ;
A7: for x being set st x in dom (f | A) holds
(f | A) . x = (f | (E /\ A)) . x

proof

let x be set ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | (E /\ A)) . x )
assume A8: x in dom (f | A) ; :: thesis: (f | A) . x = (f | (E /\ A)) . x
then (f | A) . x = f . x by FUNCT_1:70;
hence (f | A) . x = (f | (E /\ A)) . x by A6, A8, FUNCT_1:70; :: thesis: verum

end;

A9: (dom f) /\ (E /\ A) = E /\ A by A3, XBOOLE_1:17, XBOOLE_1:28;
f is_measurable_on E /\ A by A4, MESFUNC1:34, XBOOLE_1:17;
then f | (E /\ A) is_measurable_on E /\ A by A9, Th48;
then f | A is_measurable_on E /\ A by A6, A7, FUNCT_1:9;
hence 0 <= integral+ M,(f | A) by A2, A5, Th21, Th85; :: thesis: verum