let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: ( f is_simple_func_in S & g is_simple_func_in S ) and
A2: ( f is nonnegative & g is nonnegative ) and
A3: for x being set st x in dom (f - g) holds
g . x <= f . x ; :: thesis:
( dom f is Element of S & dom g is Element of S ) by A1, Th43;
then (dom f) /\ (dom g) in S by FINSUB_1:def 2;
then A4: dom (f - g) in S by A1, A2, A3, Th75;
A5: g | (dom (f - g)) is nonnegative by A2, Th21;
(- 1) (#) g is_simple_func_in S by A1, Th45;
then - g is_simple_func_in S by MESFUNC2:11;
then f + (- g) is_simple_func_in S by A1, Th44;
then A6: f - g is_simple_func_in S by MESFUNC2:9;
A7: integral' M,(f | (dom (f - g))) = (integral' M,(f - g)) + (integral' M,(g | (dom (f - g)))) by A1, A2, A3, Th75;

assume integral' M,(f | (dom (f - g))) <> +infty ; :: thesis:
f - g is nonnegative by A1, A3, Th46;
then ( 0 <= integral' M,(f - g) & 0 <= integral' M,(g | (dom (f - g))) ) by A1, A4, A5, A6, Th40, Th74;
hence integral' M,(g | (dom (f - g))) <= integral' M,(f | (dom (f - g))) by A7, XXREAL_3:42; :: thesis:

end;

hence integral' M,(g | (dom (f - g))) <= integral' M,(f | (dom (f - g))) by XXREAL_0:4; :: thesis: