theorem Th5: :: CFUNCT_1:5

for C being non empty set
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) ) )