let X be non empty set ; :: thesis: for f1, f2 being Function of X,ExtREAL st f2 is without-infty & f2 is without+infty holds
( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )
let f1, f2 be Function of X,ExtREAL; :: thesis: ( f2 is without-infty & f2 is without+infty implies ( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) ) )
assume A1: ( f2 is without-infty & f2 is without+infty ) ; :: thesis: ( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )
( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;
then A2: dom (f1 + f2) = X /\ X by A1, Th23;
hence f1 + f2 is Function of X,ExtREAL by FUNCT_2:def 1; :: thesis: for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x)
thus for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) by A2, MESFUNC1:def 3; :: thesis: verum