let f1 be PartFunc of REAL,REAL; for x0 being Real st f1 is_differentiable_in x0 holds
( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) )
let x0 be Real; ( f1 is_differentiable_in x0 implies ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) )
assume A1:
f1 is_differentiable_in x0
; ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) )
then consider N1 being Neighbourhood of x0 such that
A2:
N1 c= dom f1
and
A3:
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 FDIFF_1:def 4;
consider L1 being LinearFunc, R1 being RestFunc such that
A4:
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0))
by A3;
reconsider R = - R1 as RestFunc by Th21;
reconsider L = - L1 as LinearFunc by Th20;
A5:
L1 is total
by FDIFF_1:def 3;
consider N being Neighbourhood of x0 such that
A6:
N c= N1
;
A7:
R1 is total
by FDIFF_1:def 2;
A8:
now for x being Real st x in N holds
((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0))end;
N c= dom f1
by A2, A6, XBOOLE_1:1;
then A10:
N c= dom (- f1)
by VALUED_1:8;
hence
- f1 is_differentiable_in x0
by A8, FDIFF_1:def 4; diff ((- f1),x0) = - (diff (f1,x0))
hence diff ((- f1),x0) =
L . 1
by A10, A8, FDIFF_1:def 5
.=
- (L1 . jj)
by A5, RFUNCT_1:58
.=
- (diff (f1,x0))
by A1, A2, A4, FDIFF_1:def 5
;
verum