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

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

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

A12:
( (dom f) /\ E = E & (dom g) /\ E = E )
by A1, A2, XBOOLE_1:28;
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;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

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