let n be non zero Element of NAT ; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,(REAL n) 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 Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
let f1, f2 be PartFunc of REAL,(REAL n); :: 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 Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) ) )
A1: f1 - f2 = f1 + (- f2) by Th1;
assume that
A2: Z c= dom (f1 - f2) and
A3: f1 is_differentiable_on Z and
A4: f2 is_differentiable_on Z ; :: thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) ) )
A5: - f2 is_differentiable_on Z by A4, Th14;
hence f1 - f2 is_differentiable_on Z by A1, A2, A3, Th15; :: thesis: for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
let x be Real; :: thesis: ( x in Z implies ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) )
assume A6: x in Z ; :: thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
then A7: f2 is_differentiable_in x by A4, Th5;
thus ((f1 - f2) `| Z) . x = (diff (f1,x)) + (diff ((- f2),x)) by A1, A2, A3, A5, A6, Th15
.= (diff (f1,x)) - (diff (f2,x)) by A7, Th10 ; :: thesis: verum