theorem Th29: :: VFUNCT_2:29

for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set holds
( (- f) | X = - (f | X) & ||.f.|| | X = ||.(f | X).|| )