let a be Complex; :: thesis: 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) )
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: 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) )
let x0 be Complex; :: thesis: ( f is_differentiable_in x0 implies ( a (#) f is_differentiable_in x0 & diff (a (#) f),x0 = a * (diff f,x0) ) )
assume A1: f is_differentiable_in x0 ; :: thesis: ( a (#) f is_differentiable_in x0 & diff (a (#) f),x0 = a * (diff f,x0) )
then consider N1 being Neighbourhood of x0 such that
A2: ( N1 c= dom f & ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6;
consider L1 being C_LINEAR, R1 being C_REST such that
A3: for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A2;
reconsider L = a (#) L1 as C_LINEAR ;
reconsider R = a (#) R1 as C_REST ;
A6: N1 c= dom (a (#) f) by A2, VALUED_1:def 5;

A7: now

let x be Complex; :: thesis: ( x in N1 implies ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A8: x in N1 ; :: thesis: ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
A9: x0 in N1 by Th9;
thus ((a (#) f) /. x) - ((a (#) f) /. x0) = (a * (f /. x)) - ((a (#) f) /. x0) by A6, A8, CFUNCT_1:7
.= (a * (f /. x)) - (a * (f /. x0)) by A6, A9, CFUNCT_1:7
.= a * ((f /. x) - (f /. x0))
.= a * ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A3, A8
.= (a * (L1 /. (x - x0))) + (a * (R1 /. (x - x0)))
.= (L /. (x - x0)) + (a * (R1 /. (x - x0))) by CFUNCT_1:77
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:77 ; :: thesis: verum

end;

hence a (#) f is_differentiable_in x0 by A6, Def6; :: thesis: diff (a (#) f),x0 = a * (diff f,x0)
hence diff (a (#) f),x0 = L /. 1r by A6, A7, Def7
.= a * (L1 /. 1r ) by CFUNCT_1:77
.= a * (diff f,x0) by A1, A2, A3, Def7 ;
:: thesis: verum