let S, T be RealNormSpace; 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; 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; ( 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
; ( 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
and
A4:
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A5:
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0))
by A4;
consider N2 being Neighbourhood of x0 such that
A6:
N2 c= dom f2
and
A7:
ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc 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;
consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R2 being RestFunc of S,T such that
A8:
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0))
by A7;
reconsider R = R1 - R2 as RestFunc of S,T by Th28;
set L = L1 - L2;
consider N being Neighbourhood of x0 such that
A9:
N c= N1
and
A10:
N c= N2
by Th1;
A11:
N c= dom f2
by A6, A10;
N c= dom f1
by A3, A9;
then
N /\ N c= (dom f1) /\ (dom f2)
by A11, XBOOLE_1:27;
then A12:
N c= dom (f1 - f2)
by VFUNCT_1:def 2;
A13:
( R1 is total & R2 is total )
by Def5;
A14:
now for x being Point of S st x in N holds
((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0))end;
hence
f1 - f2 is_differentiable_in x0
by A12; diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence diff ((f1 - f2),x0) =
L1 - L2
by A12, A14, Def7
.=
(diff (f1,x0)) - L2
by A1, A3, A5, Def7
.=
(diff (f1,x0)) - (diff (f2,x0))
by A2, A6, A8, Def7
;
verum