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 A1: ( f is without-infty & g is without+infty ) ; :: thesis: f - g is without-infty
then P2: dom (f - g) = (dom f) /\ (dom g) by MESFUNC5:23;
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 B1: x in dom (f - g) ; :: thesis: -infty < (f - g) . x
then ( x in dom f & x in dom g ) by P2, XBOOLE_0:def 4;
then B2: ( -infty < f . x & g . x < +infty ) by A1, MESFUNC5:16, MESFUNC5:17;
(f - g) . x = (f . x) - (g . x) by B1, MESFUNC1:def 4;
hence -infty < (f - g) . x by B2, XXREAL_0:6, XXREAL_3:19; :: thesis: verum

end;

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