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
(f - g) . x < +infty

proof

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

end;

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