let n be non empty 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;
A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def 46;
assume that
A3: Z c= dom (f1 - f2) and
A4: f1 is_differentiable_on Z and
A5: 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)) ) )
Z c= dom f2 by A3, A2, XBOOLE_1:18;
then A6: - f2 is_differentiable_on Z by A5, Th14;
hence f1 - f2 is_differentiable_on Z by A1, A3, A4, 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 A7: x in Z ; :: thesis: ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x))
then A8: f2 is_differentiable_in x by A5, Th5;
thus ((f1 - f2) `| Z) . x = (diff (f1,x)) + (diff ((- f2),x)) by A1, A3, A4, A6, A7, Th15
.= (diff (f1,x)) - (diff (f2,x)) by A8, Th10 ; :: thesis: verum