theorem :: RFUNCT_2:19

for Y being set
for W being non empty set
for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds
h | Y is constant