:: deftheorem Def2 defines (#) VFUNCT_2:def 2 :
for X being non empty set
for V being ComplexNormSpace
for f being PartFunc of X,V
for z being Complex
for b₅ being PartFunc of X,V holds
( b₅ = z (#) f iff ( dom b₅ = dom f & ( for x being Element of X st x in dom b₅ holds
b₅ /. x = z * (f /. x) ) ) );