theorem Th52: :: VFUNCT_1:52

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