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 = (diff 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 = (diff f1,x) - (diff f2,x) ) ) )
assume that
A1: Z c= dom (f1 - f2) and
A2: f1 is_differentiable_on Z and
A3: 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 = (diff f1,x) - (diff f2,x) ) )

now

let x0 be Complex; :: thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 )
assume A4: x0 in Z ; :: thesis: f1 - f2 is_differentiable_in x0
then A5: f1 is_differentiable_in x0 by A2, Th18;
f2 is_differentiable_in x0 by A3, A4, Th18;
hence f1 - f2 is_differentiable_in x0 by A5, Th28; :: thesis: verum

end;

hence A6: f1 - f2 is_differentiable_on Z by A1, Th18; :: thesis: for x being Complex st x in Z holds
((f1 - f2) `| Z) /. x = (diff f1,x) - (diff f2,x)

now

let x be Complex; :: thesis: ( x in Z implies ((f1 - f2) `| Z) /. x = (diff f1,x) - (diff f2,x) )
assume A7: x in Z ; :: thesis: ((f1 - f2) `| Z) /. x = (diff f1,x) - (diff f2,x)
then A8: f1 is_differentiable_in x by A2, Th18;
A9: f2 is_differentiable_in x by A3, A7, Th18;
thus ((f1 - f2) `| Z) /. x = diff (f1 - f2),x by A6, A7, Def12
.= (diff f1,x) - (diff f2,x) by A8, A9, Th28 ; :: thesis: verum

end;

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