theorem :: VALUED_2:57

for X being set
for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2)