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

proof

take C = E /\ A; :: thesis: ( C = dom (f | A) & f | A is_measurable_on C )
thus dom (f | A) = C by A4, RELAT_1:61; :: thesis: f | A is_measurable_on C
A7: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;
A8: dom (f | A) = C by A4, RELAT_1:61
.= dom (f | C) by A7, RELAT_1:61 ;
A9: for x being set st x in dom (f | A) holds
(f | A) . x = (f | C) . x

proof

let x be set ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | C) . x )
assume A10: 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 A8, A10, FUNCT_1:47; :: thesis: verum

end;

f is_measurable_on C by A5, MESFUNC1:30, XBOOLE_1:17;
then f | C is_measurable_on C by A7, Th48;
hence f | A is_measurable_on C by A8, A9, FUNCT_1:2; :: thesis: verum

end;

A11: ex C being Element of S st
( C = dom (f | B) & f | B is_measurable_on C )

proof

take C = E /\ B; :: thesis: ( C = dom (f | B) & f | B is_measurable_on C )
thus dom (f | B) = C by A4, RELAT_1:61; :: thesis: f | B is_measurable_on C
A12: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;
A13: dom (f | B) = C by A4, RELAT_1:61
.= dom (f | C) by A12, RELAT_1:61 ;
A14: for x being set st x in dom (f | B) holds
(f | B) . x = (f | C) . x

proof

let x be set ; :: thesis: ( x in dom (f | B) implies (f | B) . x = (f | C) . x )
assume A15: x in dom (f | B) ; :: thesis: (f | B) . x = (f | C) . x
then (f | B) . x = f . x by FUNCT_1:47;
hence (f | B) . x = (f | C) . x by A13, A15, FUNCT_1:47; :: thesis: verum

end;

f is_measurable_on C by A5, MESFUNC1:30, XBOOLE_1:17;
then f | C is_measurable_on C by A12, Th48;
hence f | B is_measurable_on C by A13, A14, FUNCT_1:2; :: thesis: verum

end;

integral+ (M,(f | A)) <= integral+ (M,(f | B)) by A1, A2, A3, Th89;
then Integral (M,(f | A)) <= integral+ (M,(f | B)) by A2, A6, Th21, Th94;
hence Integral (M,(f | A)) <= Integral (M,(f | B)) by A2, A11, Th21, Th94; :: thesis: verum