let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis: for Z being open Subset of COMPLEX st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )
let Z be open Subset of COMPLEX; :: thesis: ( Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 (#) f2 is_differentiable_on Z & ( for x being Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) )
assume that
A1: Z c= dom (f1 (#) f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; :: thesis: ( f1 (#) f2 is_differentiable_on Z & ( for x being Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )

now :: thesis: for x0 being Complex st x0 in Z holds
f1 (#) f2 is_differentiable_in x0

let x0 be Complex; :: thesis: ( x0 in Z implies f1 (#) f2 is_differentiable_in x0 )
assume x0 in Z ; :: thesis: f1 (#) f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th15;
hence f1 (#) f2 is_differentiable_in x0 by Th26; :: thesis: verum

end;

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

now :: thesis: for x being Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x)))

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

end;

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