A1: ( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;
( {-infty} misses rng f1 & {+infty} misses rng f2 ) by ZFMISC_1:50, MESFUNC5:def 3, MESFUNC5:def 4;
then ( f1 " {-infty} = {} & f2 " {+infty} = {} ) by RELAT_1:138;
then ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) = X by A1;
then A2: dom (f1 - f2) = X by MESFUNC1:def 4;

now :: thesis: not -infty in rng (f1 - f2)

assume -infty in rng (f1 - f2) ; :: thesis: contradiction
then consider x being object such that
A3: ( x in dom (f1 - f2) & (f1 - f2) . x = -infty ) by FUNCT_1:def 3;
reconsider x = x as Element of X by A3;
(f1 - f2) . x = (f1 . x) - (f2 . x) by A3, MESFUNC1:def 4;
then ( f1 . x = -infty or f2 . x = +infty ) by A3, XXREAL_3:19;
hence contradiction by MESFUNC5:def 5, MESFUNC5:def 6; :: thesis: verum

end;

hence f1 - f2 is without-infty Function of X,ExtREAL by A2, FUNCT_2:def 1, MESFUNC5:def 3; :: thesis: verum