theorem :: VFUNCT_1:40

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