let T, S be non trivial RealNormSpace; :: thesis: for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0) )
let f1, f2 be PartFunc of S,T; :: thesis: for x0 being Point of S st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0) )
let x0 be Point of S; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0) ) )
assume that
A1:
f1 is_differentiable_in x0
and
A2:
f2 is_differentiable_in x0
; :: thesis: ( f1 - f2 is_differentiable_in x0 & diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0) )
consider N1 being Neighbourhood of x0 such that
A3:
( N1 c= dom f1 & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by A1, Def6;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R1 being REST of S,T such that
A4:
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0))
by A3;
consider N2 being Neighbourhood of x0 such that
A5:
( N2 c= dom f2 & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,T) ex R being REST of S,T st
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by A2, Def6;
consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators S,T), R2 being REST of S,T such that
A6:
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0))
by A5;
consider N being Neighbourhood of x0 such that
A7:
( N c= N1 & N c= N2 )
by Th1;
set L = L1 - L2;
reconsider R = R1 - R2 as REST of S,T by Th33;
A8:
( R1 is total & R2 is total )
by Def5;
A9:
N c= dom f1
by A3, A7, XBOOLE_1:1;
N c= dom f2
by A5, A7, XBOOLE_1:1;
then
N /\ N c= (dom f1) /\ (dom f2)
by A9, XBOOLE_1:27;
then A10:
N c= dom (f1 - f2)
by VFUNCT_1:def 2;
hence
f1 - f2 is_differentiable_in x0
by A10, Def6; :: thesis: diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0)
hence diff (f1 - f2),x0 =
L1 - L2
by A10, A11, Def7
.=
(diff f1,x0) - L2
by A1, A3, A4, Def7
.=
(diff f1,x0) - (diff f2,x0)
by A2, A5, A6, Def7
;
:: thesis: verum