theorem Th45: :: VFUNCT_1:45

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