theorem :: RFUNCT_1:77

for Y being set
for f being real-valued Function holds (0 (#) f) | Y is bounded