theorem :: VFUNCT_1:22

for C being non empty set
for r being Real
for V being non empty RealNormSpace-like NORMSTR
for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||