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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | 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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | 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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | 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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | 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
a <= f . x ) holds
a * (M . E) <= Integral (M,(f | 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
a <= f . x ) implies a * (M . E) <= Integral (M,(f | 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
a <= f . x ; :: thesis: a * (M . E) <= Integral (M,(f | E))
set C = chi (E,X);
A5: f | E is_integrable_on M by A1, MESFUNC5:97;
for x being Element of X st x in dom (a (#) ((chi (E,X)) | E)) holds
(a (#) ((chi (E,X)) | E)) . x <= (f | E) . x

proof

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

end;

then A10: (f | E) - (a (#) ((chi (E,X)) | 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 A11: dom (a (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
E = E /\ E ;
then A12: Integral (M,((chi (E,X)) | E)) = M . E by A3, MESFUNC7:25;
reconsider a = a as Real ;
chi (E,X) is_integrable_on M by A3, MESFUNC7:24;
then A13: (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
A14: E1 = (dom (f | E)) /\ (dom (a (#) ((chi (E,X)) | E))) and
A15: Integral (M,((a (#) ((chi (E,X)) | E)) | E1)) <= Integral (M,((f | E) | E1)) by A5, A10, 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 A14, A11;
hence a * (M . E) <= Integral (M,(f | E)) by A13, A15, A12, MESFUNC5:110; :: thesis: verum