let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))
let E be Element of S; :: thesis: for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))
let f, g be PartFunc of X,ExtREAL; :: thesis: ( E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) implies Integral (M,(g | E)) <= Integral (M,(f | E)) )
assume that
A1: E c= dom f and
A2: E c= dom g and
A3: ( f is E -measurable & g is E -measurable ) and
A4: f is nonpositive and
A5: for x being Element of X st x in E holds
g . x <= f . x ; :: thesis: Integral (M,(g | E)) <= Integral (M,(f | E))
set f1 = - f;
set g1 = - g;
A6: ( E c= dom (- f) & E c= dom (- g) ) by A1, A2, MESFUNC1:def 7;
A7: ( - f is E -measurable & - g is E -measurable ) by A1, A2, A3, MEASUR11:63;
A11: for x being Element of X st x in E holds
(- f) . x <= (- g) . x

proof

let x be Element of X; :: thesis: ( x in E implies (- f) . x <= (- g) . x )
assume A9: x in E ; :: thesis: (- f) . x <= (- g) . x
then ( (- f) . x = - (f . x) & (- g) . x = - (g . x) ) by A6, MESFUNC1:def 7;
hence (- f) . x <= (- g) . x by A5, A9, XXREAL_3:38; :: thesis: verum

end;

A12: ( (dom f) /\ E = E & (dom g) /\ E = E ) by A1, A2, XBOOLE_1:28;
A14: ( E = dom (f | E) & E = dom (g | E) ) by A12, RELAT_1:61;
( (- f) | E = - (f | E) & (- g) | E = - (g | E) ) by Th3;
then ( Integral (M,((- f) | E)) = - (Integral (M,(f | E))) & Integral (M,((- g) | E)) = - (Integral (M,(g | E))) ) by A3, A12, A14, Th52, MESFUNC5:42;
hence Integral (M,(g | E)) <= Integral (M,(f | E)) by A4, A6, A7, A11, XXREAL_3:38, MESFUNC9:15; :: thesis: verum