theorem :: CFUNCT_1:22
for C being non empty set
for f being PartFunc of C,COMPLEX
for r, q being Complex holds (r * q) (#) f = r (#) (q (#) f)