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 and
A3: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A4: for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = a (#) R1 as C_RestFunc ;
reconsider L = a (#) L1 as C_LinearFunc ;
A5: N1 c= dom (a (#) f) by A2, VALUED_1:def 5;

A6: now :: thesis: for x being Complex st x in N1 holds
((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0))

let x be Complex; :: thesis: ( x in N1 implies ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A7: x0 in N1 by Th7;
A8: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume A9: x in N1 ; :: thesis: ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence ((a (#) f) /. x) - ((a (#) f) /. x0) = (a * (f /. x)) - ((a (#) f) /. x0) by A5, CFUNCT_1:4
.= (a * (f /. x)) - (a * (f /. x0)) by A5, A7, CFUNCT_1:4
.= a * ((f /. x) - (f /. x0))
.= a * ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4, A9
.= (a * (L1 /. (x - x0))) + (a * (R1 /. (x - x0)))
.= (L /. (x - x0)) + (a * (R1 /. (x - x0))) by CFUNCT_1:65, A8
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:65, A8 ;
:: thesis: verum

end;

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