let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b₃ -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being b₂ -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being b₁ -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL
for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
let f be E -measurable PartFunc of X,ExtREAL; :: thesis: for er being ExtReal st dom f = E & f is nonnegative & er >= 0 holds
er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
let er be ExtReal; :: thesis: ( dom f = E & f is nonnegative & er >= 0 implies er * (M . (great_eq_dom (f,er))) <= Integral (M,f) )
assume that
A1: dom f = E and
A2: f is nonnegative and
A3: er >= 0 ; :: thesis: er * (M . (great_eq_dom (f,er))) <= Integral (M,f)
A4: great_eq_dom (f,er) c= E by A1, MESFUNC1:def 14;
A5: great_eq_dom (f,+infty) = eq_dom (f,+infty) by Th10;
( er in REAL or er = +infty ) by A3, XXREAL_0:14;
then E /\ (great_eq_dom (f,er)) is Element of S by A1, A5, MESFUNC1:27, MESFUNC1:33;
then reconsider Er = great_eq_dom (f,er) as Element of S by A4, XBOOLE_1:28;
dom (chi (er,Er,X)) = X by FUNCT_2:def 1;
then A6: ( Er = dom (f | Er) & Er = dom ((chi (er,Er,X)) | Er) ) by A1, A4, RELAT_1:62;
( f is Er -measurable & Er = Er /\ (dom f) ) by A1, A4, XBOOLE_1:28, MESFUNC1:30;
then A7: f | Er is Er -measurable by MESFUNC5:42;
A8: f | Er is nonnegative by A2, MESFUNC5:15;
A9: (chi (er,Er,X)) | Er is Er -measurable by MESFUN12:15;
chi (er,Er,X) is nonnegative by A3, MESFUN12:17;
then A10: (chi (er,Er,X)) | Er is nonnegative by MESFUNC5:15;
for x being Element of X st x in dom ((chi (er,Er,X)) | Er) holds
((chi (er,Er,X)) | Er) . x <= (f | Er) . x

proof

let x be Element of X; :: thesis: ( x in dom ((chi (er,Er,X)) | Er) implies ((chi (er,Er,X)) | Er) . x <= (f | Er) . x )
assume A11: x in dom ((chi (er,Er,X)) | Er) ; :: thesis: ((chi (er,Er,X)) | Er) . x <= (f | Er) . x
then ((chi (er,Er,X)) | Er) . x = (chi (er,Er,X)) . x by FUNCT_1:47;
then A12: ((chi (er,Er,X)) | Er) . x = er by A6, A11, MESFUN12:def 1;
A13: (f | Er) . x = f . x by A6, A11, FUNCT_1:47;
x in great_eq_dom (f,er) by A11, RELAT_1:57;
hence ((chi (er,Er,X)) | Er) . x <= (f | Er) . x by A12, A13, MESFUNC1:def 14; :: thesis: verum

end;

then integral+ (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by A6, A7, A8, A9, A10, MESFUNC5:85;
then Integral (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by A6, A10, MESFUNC5:88, MESFUN12:15;
then A14: er * (M . Er) <= integral+ (M,(f | Er)) by MESFUN12:50;
integral+ (M,(f | Er)) <= integral+ (M,(f | E)) by A1, A2, A4, MESFUNC5:83;
then integral+ (M,(f | Er)) <= Integral (M,f) by A1, A2, MESFUNC5:88;
hence er * (M . (great_eq_dom (f,er))) <= Integral (M,f) by A14, XXREAL_0:2; :: thesis: verum