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, b being real number 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 & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (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, b being real number 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 & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (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, b being real number 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 & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . E) )
let f be PartFunc of X,ExtREAL ; :: thesis: for E being Element of S
for a, b being real number 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 & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . E) )
let E be Element of S; :: thesis: for a, b being real number 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 & f . x <= b ) ) holds
( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . E) )
let a, b be real number ; :: 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 & f . x <= b ) ) implies ( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . E) ) )
reconsider a1 = a, b1 = b as Element of REAL by XREAL_0:def 1;
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 & f . x <= b ) ; :: thesis: ( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . 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, Th24;
then A6: (chi E,X) | E is_integrable_on M by MESFUNC5:103;
then A7: ( a1 (#) ((chi E,X) | E) is_integrable_on M & b1 (#) ((chi E,X) | E) is_integrable_on M ) by MESFUNC5:116;
for x being Element of X st x in dom (a1 (#) ((chi E,X) | E)) holds
(a1 (#) ((chi E,X) | E)) . x <= (f | E) . x

proof

let x be Element of X; :: thesis: ( x in dom (a1 (#) ((chi E,X) | E)) implies (a1 (#) ((chi E,X) | E)) . x <= (f | E) . x )
assume A8: x in dom (a1 (#) ((chi E,X) | E)) ; :: thesis: (a1 (#) ((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;
(a1 (#) ((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 (a1 (#) ((chi E,X) | E)) . x <= (f | E) . x by A11, XXREAL_3:92; :: thesis: verum

end;

then (f | E) - (a1 (#) ((chi E,X) | E)) is nonnegative by Th1;
then consider E1 being Element of S such that
A12: ( E1 = (dom (f | E)) /\ (dom (a1 (#) ((chi E,X) | E))) & Integral M,((a1 (#) ((chi E,X) | E)) | E1) <= Integral M,((f | E) | E1) ) by A5, A7, Th3;
dom (f | E) = (dom f) /\ E by RELAT_1:90;
then A13: dom (f | E) = E by A2, XBOOLE_1:28;
( dom (a1 (#) ((chi E,X) | E)) = dom ((chi E,X) | E) & dom (b1 (#) ((chi E,X) | E)) = dom ((chi E,X) | E) ) by MESFUNC1:def 6;
then ( dom (a1 (#) ((chi E,X) | E)) = (dom (chi E,X)) /\ E & dom (b1 (#) ((chi E,X) | E)) = (dom (chi E,X)) /\ E ) by RELAT_1:90;
then ( dom (a1 (#) ((chi E,X) | E)) = X /\ E & dom (b1 (#) ((chi E,X) | E)) = X /\ E ) by FUNCT_3:def 3;
then A14: ( dom (a1 (#) ((chi E,X) | E)) = E & dom (b1 (#) ((chi E,X) | E)) = E ) by XBOOLE_1:28;
for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (b1 (#) ((chi E,X) | E)) . x

proof

let x be Element of X; :: thesis: ( x in dom (f | E) implies (f | E) . x <= (b1 (#) ((chi E,X) | E)) . x )
assume A15: x in dom (f | E) ; :: thesis: (f | E) . x <= (b1 (#) ((chi E,X) | E)) . x
then A16: x in dom ((chi E,X) | E) by A13, A14, MESFUNC1:def 6;
then x in (dom (chi E,X)) /\ E by RELAT_1:90;
then A17: ( x in dom (chi E,X) & x in E ) by XBOOLE_0:def 4;
then f . x <= b by A4;
then A18: (f | E) . x <= b by A17, FUNCT_1:72;
(b1 (#) ((chi E,X) | E)) . x = (R_EAL b) * (((chi E,X) | E) . x) by A13, A14, A15, MESFUNC1:def 6
.= (R_EAL b) * ((chi E,X) . x) by A16, FUNCT_1:70
.= (R_EAL b) * 1. by A17, FUNCT_3:def 3 ;
hence (f | E) . x <= (b1 (#) ((chi E,X) | E)) . x by A18, XXREAL_3:92; :: thesis: verum

end;

then (b1 (#) ((chi E,X) | E)) - (f | E) is nonnegative by Th1;
then consider E2 being Element of S such that
A19: ( E2 = (dom (f | E)) /\ (dom (b1 (#) ((chi E,X) | E))) & Integral M,((f | E) | E2) <= Integral M,((b1 (#) ((chi E,X) | E)) | E2) ) by A5, A7, Th3;
A20: ( (a1 (#) ((chi E,X) | E)) | E1 = a1 (#) ((chi E,X) | E) & (b1 (#) ((chi E,X) | E)) | E2 = b1 (#) ((chi E,X) | E) & (f | E) | E1 = f | E & (f | E) | E2 = f | E ) by A12, A13, A14, A19, RELAT_1:98;
E = E /\ E ;
then Integral M,((chi E,X) | E) = M . E by A3, Th25;
hence ( (R_EAL a) * (M . E) <= Integral M,(f | E) & Integral M,(f | E) <= (R_EAL b) * (M . E) ) by A6, A12, A19, A20, MESFUNC5:116; :: thesis: verum