let f1, f2 be PartFunc of COMPLEX,COMPLEX; 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; ( 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 )
; ( 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))) ) )
hence A3:
f1 (#) f2 is_differentiable_on Z
by A1, Th15; for x being Complex st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x)))
now 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;
( x in Z implies ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) )assume A4:
x in Z
;
((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
;
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)))
; verum