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 E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S
for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)
let E be Element of S; :: thesis: for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) holds
Integral (M,(f | E)) <= a * (M . E)
let a be Real; :: thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds
f . x <= a ) implies Integral (M,(f | E)) <= a * (M . E) )
assume that
A1: f is_integrable_on M and
A2: E c= dom f and
A3: M . E < +infty and
A4: for x being Element of X st x in E holds
f . x <= a ; :: thesis: Integral (M,(f | E)) <= a * (M . E)
set C = chi (E,X);
A5: f | E is_integrable_on M by A1, MESFUNC5:97;
dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def 6;
then dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61;
then dom (a (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def 3;
then A6: dom (a (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
dom (f | E) = (dom f) /\ E by RELAT_1:61;
then A7: dom (f | E) = E by A2, XBOOLE_1:28;
for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (a (#) ((chi (E,X)) | E)) . x

proof

let x be Element of X; :: thesis: ( x in dom (f | E) implies (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x )
assume A8: x in dom (f | E) ; :: thesis: (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x
then A9: x in dom ((chi (E,X)) | E) by A7, A6, MESFUNC1:def 6;
then x in (dom (chi (E,X))) /\ E by RELAT_1:61;
then A10: x in E by XBOOLE_0:def 4;
then f . x <= a by A4;
then A11: (f | E) . x <= a by A10, FUNCT_1:49;
(a (#) ((chi (E,X)) | E)) . x = a * (((chi (E,X)) | E) . x) by A7, A6, A8, MESFUNC1:def 6
.= a * ((chi (E,X)) . x) by A9, FUNCT_1:47
.= a * 1. by A10, FUNCT_3:def 3 ;
hence (f | E) . x <= (a (#) ((chi (E,X)) | E)) . x by A11, XXREAL_3:81; :: thesis: verum

end;

then A12: (a (#) ((chi (E,X)) | E)) - (f | E) is nonnegative by MESFUNC7:1;
dom (a (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def 6;
then dom (a (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61;
then dom (a (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def 3;
then A13: dom (a (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
E = E /\ E ;
then A14: Integral (M,((chi (E,X)) | E)) = M . E by A3, MESFUNC7:25;
chi (E,X) is_integrable_on M by A3, MESFUNC7:24;
then A15: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97;
then a (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110;
then consider E1 being Element of S such that
A16: E1 = (dom (f | E)) /\ (dom (a (#) ((chi (E,X)) | E))) and
A17: Integral (M,((f | E) | E1)) <= Integral (M,((a (#) ((chi (E,X)) | E)) | E1)) by A5, A12, MESFUNC7:3;
dom (f | E) = (dom f) /\ E by RELAT_1:61;
then dom (f | E) = E by A2, XBOOLE_1:28;
then ( (a (#) ((chi (E,X)) | E)) | E1 = a (#) ((chi (E,X)) | E) & (f | E) | E1 = f | E ) by A16, A13;
hence Integral (M,(f | E)) <= a * (M . E) by A15, A17, A14, MESFUNC5:110; :: thesis: verum