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 b3 -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 b2 -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 b1 -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 ;
A5: great_eq_dom (f,+infty) = eq_dom (f,+infty) by Th10;
( er in REAL or er = +infty ) by ;
then E /\ (great_eq_dom (f,er)) is Element of S by ;
then reconsider Er = great_eq_dom (f,er) as Element of S by ;
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 ;
( f is Er -measurable & Er = Er /\ (dom f) ) by ;
then A7: f | Er is Er -measurable by MESFUNC5:42;
A8: f | Er is nonnegative by ;
A9: (chi (er,Er,X)) | Er is Er -measurable by MESFUN12:15;
chi (er,Er,X) is V97() by ;
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 ;
A13: (f | Er) . x = f . x by ;
x in great_eq_dom (f,er) by ;
hence ((chi (er,Er,X)) | Er) . x <= (f | Er) . x by ; :: thesis: verum
end;
then integral+ (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by ;
then Integral (M,((chi (er,Er,X)) | Er)) <= integral+ (M,(f | Er)) by ;
then A14: er * (M . Er) <= integral+ (M,(f | Er)) by MESFUN12:50;
integral+ (M,(f | Er)) <= integral+ (M,(f | E)) by ;
then integral+ (M,(f | Er)) <= Integral (M,f) by ;
hence er * (M . (great_eq_dom (f,er))) <= Integral (M,f) by ; :: thesis: verum