theorem Th25: :: CFDIFF_1:25

for a being Complex
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Complex st f is_differentiable_in x0 holds
( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )