let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let f, g be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: E c= dom f and
A2: E c= dom g and
A3: f is E -measurable and
A4: g is E -measurable and
A5: f is nonnegative and
A6: for x being Element of X st x in E holds
f . x <= g . x ; :: thesis:
set F2 = g | E;
A7: E = dom (f | E) by A1, RELAT_1:62;
set F1 = f | E;
A8: f | E is nonnegative by A5, MESFUNC5:15;
A9: E = dom (g | E) by A2, RELAT_1:62;
A10: for x being Element of X st x in dom (f | E) holds
(f | E) . x <= (g | E) . x

let x be Element of X; :: thesis:
assume A11: x in dom (f | E) ; :: thesis:
then A12: (f | E) . x = f . x by FUNCT_1:47;
(g | E) . x = g . x by A7, A9, A11, FUNCT_1:47;
hence (f | E) . x <= (g | E) . x by A6, A7, A11, A12; :: thesis:

end;

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

let x be object ; :: thesis:
assume A13: x in dom (g | E) ; :: thesis:
0 <= (f | E) . x by A8, SUPINF_2:51;
hence 0 <= (g | E) . x by A7, A9, A10, A13; :: thesis:

end;

then A14: g | E is nonnegative by SUPINF_2:52;
A15: (dom g) /\ E = E by A2, XBOOLE_1:28;
then A16: g | E is E -measurable by A4, MESFUNC5:42;
A17: (dom f) /\ E = E by A1, XBOOLE_1:28;
then f | E is E -measurable by A3, MESFUNC5:42;
then integral+ (M,(f | E)) <= integral+ (M,(g | E)) by A8, A7, A9, A10, A14, A16, MESFUNC5:85;
then Integral (M,(f | E)) <= integral+ (M,(g | E)) by A3, A8, A7, A17, MESFUNC5:42, MESFUNC5:88;
hence Integral (M,(f | E)) <= Integral (M,(g | E)) by A4, A9, A14, A15, MESFUNC5:42, MESFUNC5:88; :: thesis: