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

( 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

hence
f - g is nonnegative
by SUPINF_2:52; :: thesis: verum0 <= (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;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