theorem :: CFUNCT_1:82

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