theorem Th29: :: VFUNCT_1:29

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