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 set st x in dom (f - g) holds
g . x <= f . x ; :: thesis:
( f is without+infty & g is without-infty ) by A1, A2, Th20;
then ( not +infty in rng f & not -infty in rng g ) by Def3, Def4;
then A4: ( f " {+infty } = {} & g " {-infty } = {} ) by FUNCT_1:142;
then ((dom f) /\ (dom g)) \ (((f " {+infty }) /\ (g " {+infty })) \/ ((f " {-infty }) /\ (g " {-infty }))) = (dom f) /\ (dom g) ;
then A5: 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 A6: x in (dom f) /\ (dom g) ; :: thesis:
hence g . x <= f . x by A3, A5; :: thesis:
A7: ( x in dom f & x in dom g ) by A6, XBOOLE_0:def 4;
then not g . x in {-infty } by A4, FUNCT_1:def 13;
then not g . x = -infty by TARSKI:def 1;
hence -infty < g . x by XXREAL_0:6; :: thesis:
not f . x in {+infty } by A4, A7, FUNCT_1:def 13;
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 Th27; :: thesis: