theorem :: CFUNCT_1:66

for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )