let S, T be 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 and
A4: ex L being Point of 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 , 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 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 , 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 ;
N c= dom f1 by A3, A9;
then N /\ N c= (dom f1) /\ (dom f2) by ;
then A12: N c= dom (f1 - f2) by VFUNCT_1:def 2;
A13: ( R1 is total & R2 is total ) by Def5;
A14: now :: thesis: for x being Point of S st x in N holds
((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0))
let x be Point of S; :: thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0)) )
A15: x0 in N by NFCONT_1:4;
assume A16: x in N ; :: thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((L1 - L2) . (x - x0)) + (R /. (x - x0))
hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by
.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by
.= (((f1 /. x) - (f2 /. x)) - (f1 /. x0)) + (f2 /. x0) by RLVECT_1:29
.= ((f1 /. x) - ((f1 /. x0) + (f2 /. x))) + (f2 /. x0) by RLVECT_1:27
.= (((f1 /. x) - (f1 /. x0)) - (f2 /. x)) + (f2 /. x0) by RLVECT_1:27
.= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)) by RLVECT_1:29
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A9, A16
.= ((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0))) by A8, A10, A16
.= (((L1 . (x - x0)) + (R1 /. (x - x0))) - (L2 . (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:27
.= ((L1 . (x - x0)) + ((R1 /. (x - x0)) + (- (L2 . (x - x0))))) - (R2 /. (x - x0)) by RLVECT_1:def 3
.= ((L1 . (x - x0)) - ((L2 . (x - x0)) - (R1 /. (x - x0)))) - (R2 /. (x - x0)) by RLVECT_1:33
.= (((L1 . (x - x0)) - (L2 . (x - x0))) + (R1 /. (x - x0))) - (R2 /. (x - x0)) by RLVECT_1:29
.= ((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by RLVECT_1:def 3
.= ((L1 - L2) . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by LOPBAN_1:40
.= ((L1 - L2) . (x - x0)) + (R /. (x - x0)) by ;
:: thesis: verum
end;
hence f1 - f2 is_differentiable_in x0 by A12; :: thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence diff ((f1 - f2),x0) = L1 - L2 by
.= (diff (f1,x0)) - L2 by A1, A3, A5, Def7
.= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def7 ;
:: thesis: verum