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_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral M,(f | E) <= Integral M,(g | 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_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral M,(f | E) <= Integral M,(g | 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_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral M,(f | E) <= Integral M,(g | 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_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral M,(f | E) <= Integral M,(g | E)
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds
f . x <= g . x ) implies Integral M,(f | E) <= Integral M,(g | E) )
assume that
A0: ( E c= dom f & E c= dom g ) and
A2: ( f is_measurable_on E & g is_measurable_on E ) and
A3: f is nonnegative and
A4: for x being Element of X st x in E holds
f . x <= g . x ; :: thesis: Integral M,(f | E) <= Integral M,(g | E)
set F1 = f | E;
set F2 = g | E;
A5: f | E is nonnegative by A3, MESFUNC5:21;
A6: ( E = dom (f | E) & E = dom (g | E) ) by A0, RELAT_1:91;
A7: for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (g | E) . x

proof

let x be Element of X; :: thesis: ( x in dom (f | E) implies (f | E) . x <= (g | E) . x )
assume E4: x in dom (f | E) ; :: thesis: (f | E) . x <= (g | E) . x
then ( (f | E) . x = f . x & (g | E) . x = g . x ) by A6, FUNCT_1:70;
hence (f | E) . x <= (g | E) . x by E4, A4, A6; :: thesis: verum

end;

for x being set st x in dom (g | E) holds
0 <= (g | E) . x

proof

let x be set ; :: thesis: ( x in dom (g | E) implies 0 <= (g | E) . x )
assume x in dom (g | E) ; :: thesis: 0 <= (g | E) . x
then ( 0 <= (f | E) . x & (f | E) . x <= (g | E) . x ) by A6, A5, A7, SUPINF_2:70;
hence 0 <= (g | E) . x ; :: thesis: verum

end;

then A8: g | E is nonnegative by SUPINF_2:71;
A9: ( (dom f) /\ E = E & (dom g) /\ E = E ) by A0, XBOOLE_1:28;
then ( f | E is_measurable_on E & g | E is_measurable_on E ) by A2, MESFUNC5:48;
then integral+ M,(f | E) <= integral+ M,(g | E) by A5, A7, A8, A6, MESFUNC5:91;
then Integral M,(f | E) <= integral+ M,(g | E) by A5, A6, A9, A2, MESFUNC5:48, MESFUNC5:94;
hence Integral M,(f | E) <= Integral M,(g | E) by A8, A6, A2, A9, MESFUNC5:48, MESFUNC5:94; :: thesis: verum