let X be non empty set ; :: thesis: for f being Function of X,ExtREAL holds f + (X --> 0.) = f
let f be Function of X,ExtREAL; :: thesis: f + (X --> 0.) = f
dom f = X by FUNCT_2:def 1;
hence f + (X --> 0.) = f by MESFUN11:27; :: thesis: verum