theorem :: VFUNCT_1:55

for Y being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is constant holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )