theorem Th89: :: RFUNCT_1:89

for Y being set
for C being non empty set
for p being Real
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant