theorem Th80: :: CFUNCT_1:81

for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
f | Y is bounded