for a being Complex
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds
( a (#) f is_differentiable_on Z & ( for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )