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

end;

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