theorem Th53: :: VFUNCT_2:53

for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant & (- f) | Y is constant )