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 and
A2: g is_simple_func_in S and
A3: for x being object st x in dom (f - g) holds
g . x <= f . x ; :: thesis:
g is () by A2, Th14;
then not -infty in rng g ;
then A4: g " {-infty} = {} by FUNCT_1:72;
f is () by A1, Th14;
then not +infty in rng f ;
then A5: f " {+infty} = {} by FUNCT_1:72;
then ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) = (dom f) /\ (dom g) by A4;
then A6: dom (f - g) = (dom f) /\ (dom g) by MESFUNC1:def 4;
for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x & -infty < g . x & f . x < +infty )

let x be set ; :: thesis:
assume A7: x in (dom f) /\ (dom g) ; :: thesis:
hence g . x <= f . x by A3, A6; :: thesis:
x in dom g by A7, XBOOLE_0:def 4;
then not g . x in {-infty} by A4, FUNCT_1:def 7;
then not g . x = -infty by TARSKI:def 1;
hence -infty < g . x by XXREAL_0:6; :: thesis:
x in dom f by A7, XBOOLE_0:def 4;
then not f . x in {+infty} by A5, FUNCT_1:def 7;
then not f . x = +infty by TARSKI:def 1;
hence f . x < +infty by XXREAL_0:4; :: thesis:

end;

hence f - g is nonnegative by Th21; :: thesis: