theorem :: CFUNCT_1:31

for C being non empty set
for f being PartFunc of C,COMPLEX holds - f = (- 1r) (#) f by COMPLEX1:def 4;