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;

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

hence
- f is constant
by PARTFUN2:def 1; :: thesis: verumfor 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;(- 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