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
(R_EAL 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
(R_EAL 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
(R_EAL 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
(R_EAL 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
(R_EAL 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 (R_EAL 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: (R_EAL a) * (M . E) <= Integral M,(f | E)
set C = chi E,X;
A5: f | E is_integrable_on M by A1, MESFUNC5:103;
chi E,X is_integrable_on M by A3, MESFUNC7:24;
then A6: (chi E,X) | E is_integrable_on M by MESFUNC5:103;
then A7: a (#) ((chi E,X) | E) is_integrable_on M by MESFUNC5:116;
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 A8: x in dom (a (#) ((chi E,X) | E)) ; :: thesis: (a (#) ((chi E,X) | E)) . x <= (f | E) . x
then A9: x in dom ((chi E,X) | E) by MESFUNC1:def 6;
then x in (dom (chi E,X)) /\ E by RELAT_1:90;
then A10: ( x in dom (chi E,X) & x in E ) by XBOOLE_0:def 4;
then a <= f . x by A4;
then A11: a <= (f | E) . x by A10, FUNCT_1:72;
(a (#) ((chi E,X) | E)) . x = (R_EAL a) * (((chi E,X) | E) . x) by A8, MESFUNC1:def 6
.= (R_EAL a) * ((chi E,X) . x) by A9, FUNCT_1:70
.= (R_EAL a) * 1. by A10, FUNCT_3:def 3 ;
hence (a (#) ((chi E,X) | E)) . x <= (f | E) . x by A11, XXREAL_3:92; :: thesis: verum

end;

then (f | E) - (a (#) ((chi E,X) | E)) is nonnegative by MESFUNC7:1;
then consider E1 being Element of S such that
A12: ( E1 = (dom (f | E)) /\ (dom (a (#) ((chi E,X) | E))) & Integral M,((a (#) ((chi E,X) | E)) | E1) <= Integral M,((f | E) | E1) ) by A5, A7, MESFUNC7:3;
dom (f | E) = (dom f) /\ E by RELAT_1:90;
then A13: dom (f | E) = E by A2, XBOOLE_1:28;
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:90;
then dom (a (#) ((chi E,X) | E)) = X /\ E by FUNCT_3:def 3;
then A14: dom (a (#) ((chi E,X) | E)) = E by XBOOLE_1:28;
A20: ( (a (#) ((chi E,X) | E)) | E1 = a (#) ((chi E,X) | E) & (f | E) | E1 = f | E ) by A12, A13, A14, RELAT_1:98;
E = E /\ E ;
then Integral M,((chi E,X) | E) = M . E by A3, MESFUNC7:25;
hence (R_EAL a) * (M . E) <= Integral M,(f | E) by A6, A12, A20, MESFUNC5:116; :: thesis: verum