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_measurable_on E and
A4: g is_measurable_on E 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:91;
set F1 = f | E;
A8: f | E is nonnegative by A5, MESFUNC5:21;
A9: E = dom (g | E) by A2, RELAT_1:91;
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:70;
(g | E) . x = g . x by A7, A9, A11, FUNCT_1:70;
hence (f | E) . x <= (g | E) . x by A6, A7, A11, A12; :: thesis:

end;

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

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

end;

then A14: g | E is nonnegative by SUPINF_2:71;
A15: (dom g) /\ E = E by A2, XBOOLE_1:28;
then A16: g | E is_measurable_on E by A4, MESFUNC5:48;
A17: (dom f) /\ E = E by A1, XBOOLE_1:28;
then f | E is_measurable_on E by A3, MESFUNC5:48;
then integral+ M,(f | E) <= integral+ M,(g | E) by A8, A7, A9, A10, A14, A16, MESFUNC5:91;
then Integral M,(f | E) <= integral+ M,(g | E) by A3, A8, A7, A17, MESFUNC5:48, MESFUNC5:94;
hence Integral M,(f | E) <= Integral M,(g | E) by A4, A9, A14, A15, MESFUNC5:48, MESFUNC5:94; :: thesis: