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 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
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= 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 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
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= 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 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
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S
for a, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let E be Element of S; :: thesis: for a, b 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 & f . x <= b ) ) holds
( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) )
let a, b 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 & f . x <= b ) ) implies ( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= 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: ( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . 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 (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 A6: x in dom (a1 (#) ((chi (E,X)) | E)) ; :: thesis: (a1 (#) ((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;
(a1 (#) ((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 (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x by A9, XXREAL_3:81; :: thesis: verum

end;

then A10: (f | E) - (a1 (#) ((chi (E,X)) | E)) is nonnegative by Th1;
chi (E,X) is_integrable_on M by A3, Th24;
then A11: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97;
then a1 (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110;
then consider E1 being Element of S such that
A12: E1 = (dom (f | E)) /\ (dom (a1 (#) ((chi (E,X)) | E))) and
A13: Integral (M,((a1 (#) ((chi (E,X)) | E)) | E1)) <= Integral (M,((f | E) | E1)) by A5, A10, Th3;
dom (f | E) = (dom f) /\ E by RELAT_1:61;
then A14: dom (f | E) = E by A2, XBOOLE_1:28;
dom (a1 (#) ((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 by RELAT_1:61;
then dom (a1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def 3;
then A15: dom (a1 (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28;
then A16: (f | E) | E1 = f | E by A12, A14, RELAT_1:69;
dom (b1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def 6;
then dom (b1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61;
then dom (b1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def 3;
then A17: 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 A18: x in dom (f | E) ; :: thesis: (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x
then A19: x in dom ((chi (E,X)) | E) by A14, A15, MESFUNC1:def 6;
then x in (dom (chi (E,X))) /\ E by RELAT_1:61;
then A20: x in E by XBOOLE_0:def 4;
then f . x <= b by A4;
then A21: (f | E) . x <= b by A20, FUNCT_1:49;
(b1 (#) ((chi (E,X)) | E)) . x = b * (((chi (E,X)) | E) . x) by A14, A17, A18, MESFUNC1:def 6
.= b * ((chi (E,X)) . x) by A19, FUNCT_1:47
.= b * 1. by A20, FUNCT_3:def 3 ;
hence (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x by A21, XXREAL_3:81; :: thesis: verum

end;

then A22: (b1 (#) ((chi (E,X)) | E)) - (f | E) is nonnegative by Th1;
b1 (#) ((chi (E,X)) | E) is_integrable_on M by A11, MESFUNC5:110;
then consider E2 being Element of S such that
A23: E2 = (dom (f | E)) /\ (dom (b1 (#) ((chi (E,X)) | E))) and
A24: Integral (M,((f | E) | E2)) <= Integral (M,((b1 (#) ((chi (E,X)) | E)) | E2)) by A5, A22, Th3;
A25: (b1 (#) ((chi (E,X)) | E)) | E2 = b1 (#) ((chi (E,X)) | E) by A14, A17, A23, RELAT_1:69;
E = E /\ E ;
then A26: Integral (M,((chi (E,X)) | E)) = M . E by A3, Th25;
A27: (f | E) | E2 = f | E by A14, A17, A23, RELAT_1:69;
(a1 (#) ((chi (E,X)) | E)) | E1 = a1 (#) ((chi (E,X)) | E) by A12, A14, A15, RELAT_1:69;
hence ( a * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= b * (M . E) ) by A11, A13, A24, A25, A16, A27, A26, MESFUNC5:110; :: thesis: verum