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 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 3;

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 3;
then ( f1 . x = +infty or f2 . x = +infty ) by A3, XXREAL_3:16;
hence contradiction by MESFUNC5:def 6; :: thesis: verum

end;

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