dom (- f) = dom f by MESFUNC1:def 7;
then A1: dom (- f) = X by FUNCT_2:def 1;

now :: thesis: for x being object st x in X holds
(- f) . x in ExtREAL

let x be object ; :: thesis: ( x in X implies (- f) . x in ExtREAL )
assume x in X ; :: thesis: (- f) . x in ExtREAL
then reconsider x1 = x as Element of X ;
(- f) . x = - (f . x1) by A1, MESFUNC1:def 7;
hence (- f) . x in ExtREAL ; :: thesis: verum

end;

hence - f is Function of X,ExtREAL by A1, FUNCT_2:3; :: thesis: verum