let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX holds
( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
let f be PartFunc of C,COMPLEX; :: thesis: ( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
thus A1: dom (- f) = dom f by VALUED_1:8; :: thesis: for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c)

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

let c be Element of C; :: thesis: ( c in dom (- f) implies (- f) /. c = - (f /. c) )
assume A2: c in dom (- f) ; :: thesis: (- f) /. c = - (f /. c)
hence (- f) /. c = (- f) . c by PARTFUN1:def 6
.= - (f . c) by VALUED_1:8
.= - (f /. c) by A1, A2, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ; :: thesis: verum