let x0 be Real; for f1, f2 being PartFunc of REAL,REAL 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 REAL,REAL; ( 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)) ) )
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
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 LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0))
by A1;
consider L1 being LinearFunc, R1 being RestFunc such that
A5:
for x being Real 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 LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0))
by A2;
consider L2 being LinearFunc, R2 being RestFunc such that
A8:
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L2 . (x - x0)) + (R2 . (x - x0))
by A7;
reconsider R = R1 - R2 as RestFunc by Th4;
reconsider L = L1 - L2 as LinearFunc by Th2;
A9:
( L1 is total & L2 is total )
by Def3;
consider N being Neighbourhood of x0 such that
A10:
N c= N1
and
A11:
N c= N2
by RCOMP_1:17;
A12:
N c= dom f2
by A6, A11;
N c= dom f1
by A3, A10;
then
N /\ N c= (dom f1) /\ (dom f2)
by A12, XBOOLE_1:27;
then A13:
N c= dom (f1 - f2)
by VALUED_1:12;
A14:
( R1 is total & R2 is total )
by Def2;
A15:
now for x being Real st x in N holds
((f1 - f2) . x) - ((f1 - f2) . x0) = (L . (x - x0)) + (R . (x - x0))let x be
Real;
( x in N implies ((f1 - f2) . x) - ((f1 - f2) . x0) = (L . (x - x0)) + (R . (x - x0)) )A16:
x0 in N
by RCOMP_1:16;
reconsider xx =
x,
xx0 =
x0 as
Element of
REAL by XREAL_0:def 1;
assume A17:
x in N
;
((f1 - f2) . x) - ((f1 - f2) . x0) = (L . (x - x0)) + (R . (x - x0))hence ((f1 - f2) . x) - ((f1 - f2) . x0) =
((f1 . x) - (f2 . x)) - ((f1 - f2) . x0)
by A13, VALUED_1:13
.=
((f1 . x) - (f2 . x)) - ((f1 . x0) - (f2 . x0))
by A13, A16, VALUED_1:13
.=
((f1 . x) - (f1 . x0)) - ((f2 . x) - (f2 . x0))
.=
((L1 . (x - x0)) + (R1 . (x - x0))) - ((f2 . x) - (f2 . x0))
by A5, A10, A17
.=
((L1 . (x - x0)) + (R1 . (x - x0))) - ((L2 . (x - x0)) + (R2 . (x - x0)))
by A8, A11, A17
.=
((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 . (x - x0)) - (R2 . (x - x0)))
.=
(L . (xx - xx0)) + ((R1 . (xx - xx0)) - (R2 . (xx - xx0)))
by A9, RFUNCT_1:56
.=
(L . (x - x0)) + (R . (x - x0))
by A14, RFUNCT_1:56
;
verum end;
hence
f1 - f2 is_differentiable_in x0
by A13; diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence diff ((f1 - f2),x0) =
L . 1
by A13, A15, Def5
.=
(L1 . j) - (L2 . j)
by A9, RFUNCT_1:56
.=
(diff (f1,x0)) - (L2 . 1)
by A1, A3, A5, Def5
.=
(diff (f1,x0)) - (diff (f2,x0))
by A2, A6, A8, Def5
;
verum