theorem :: VFUNCT_1:34

for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds
( f is total iff r (#) f is total ) by Def4;