let X be non empty set ; :: thesis: for f, g being PartFunc of X,ExtREAL st ( for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x & -infty < g . x & f . x < +infty ) ) holds
f - g is nonnegative
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x & -infty < g . x & f . x < +infty ) ) implies f - g is nonnegative )
assume A1: for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x & -infty < g . x & f . x < +infty ) ; :: thesis: f - g is nonnegative

now :: thesis: for x being object st x in dom (f - g) holds
0 <= (f - g) . x

let x be object ; :: thesis: ( x in dom (f - g) implies 0 <= (f - g) . x )
assume A2: x in dom (f - g) ; :: thesis: 0 <= (f - g) . x
dom (f - g) = ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) by MESFUNC1:def 4;
then dom (f - g) c= (dom f) /\ (dom g) by XBOOLE_1:36;
then 0 <= (f . x) - (g . x) by A1, A2, XXREAL_3:40;
hence 0 <= (f - g) . x by A2, MESFUNC1:def 4; :: thesis: verum

end;

hence f - g is nonnegative by SUPINF_2:52; :: thesis: verum