let a be Complex; :: thesis: 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) ) )
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: 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) ) )
let Z be open Subset of COMPLEX ; :: thesis: ( Z c= dom (a (#) f) & f is_differentiable_on Z implies ( a (#) f is_differentiable_on Z & ( for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff f,x) ) ) )
assume that
A1: Z c= dom (a (#) f) and
A2: f is_differentiable_on Z ; :: thesis: ( a (#) f is_differentiable_on Z & ( for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff f,x) ) )

now

let x0 be Complex; :: thesis: ( x0 in Z implies a (#) f is_differentiable_in x0 )
assume x0 in Z ; :: thesis: a (#) f is_differentiable_in x0
then f is_differentiable_in x0 by A2, Th15;
hence a (#) f is_differentiable_in x0 by Th25; :: thesis: verum

end;

hence A3: a (#) f is_differentiable_on Z by A1, Th15; :: thesis: for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff f,x)

now

let x be Complex; :: thesis: ( x in Z implies ((a (#) f) `| Z) /. x = a * (diff f,x) )
assume A4: x in Z ; :: thesis: ((a (#) f) `| Z) /. x = a * (diff f,x)
then A5: f is_differentiable_in x by A2, Th15;
thus ((a (#) f) `| Z) /. x = diff (a (#) f),x by A3, A4, Def12
.= a * (diff f,x) by A5, Th25 ; :: thesis: verum

end;

hence for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff f,x) ; :: thesis: verum