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 :: thesis: for x0 being Complex st x0 in Z holds
a (#) f is_differentiable_in x0

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 :: thesis: for x being Complex st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x))

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