theorem :: VALUED_2:53

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)