for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)