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 (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;

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 ;

:: thesis: verum

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 (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 :: 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))

hence
f1 - f2 is_differentiable_in x0
by A12; :: thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))((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 A12, VFUNCT_1:def 2

.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A15, VFUNCT_1:def 2

.= (((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 A13, VFUNCT_1:37 ;

:: thesis: verum

end;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 A12, VFUNCT_1:def 2

.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A15, VFUNCT_1:def 2

.= (((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 A13, VFUNCT_1:37 ;

:: thesis: verum

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 ;

:: thesis: verum