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

proof

let x be set ; :: thesis: ( x in dom (f - g) implies -infty < (f - g) . x )
assume A3: x in dom (f - g) ; :: thesis: -infty < (f - g) . x
A4: -infty < f . x by A1;
A5: g . x < +infty by A2;
(f - g) . x = (f . x) - (g . x) by A3, MESFUNC1:def 4;
hence -infty < (f - g) . x by A4, A5, XXREAL_0:6, XXREAL_3:19; :: thesis: verum

end;

hence f - g is without-infty by MESFUNC5:10; :: thesis: verum