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
( ( for z being Complex holds z (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )