consider r being Element of REAL such that
A1: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def 1;

now :: thesis: ex p being Element of REAL st
for c being Element of C st c in dom (- f) holds
(- f) . c = p

take p = - r; :: thesis: for c being Element of C st c in dom (- f) holds
(- f) . c = p
let c be Element of C; :: thesis: ( c in dom (- f) implies (- f) . c = p )
assume c in dom (- f) ; :: thesis: (- f) . c = p
then c in dom f by VALUED_1:8;
then - (f . c) = p by A1;
hence (- f) . c = p by VALUED_1:8; :: thesis: verum

end;

hence - f is constant by PARTFUN2:def 1; :: thesis: verum