theorem Th14: :: VFUNCT_1:14

for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r, p being Real holds (r * p) (#) f = r (#) (p (#) f)