theorem :: VFUNCT_2:38

for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)