let f1 be PartFunc of REAL,REAL; :: thesis: 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; :: thesis: ( f1 is_differentiable_in x0 implies ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) )
assume A1: f1 is_differentiable_in x0 ; :: thesis: ( - 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 :: thesis: for x being Real st x in N holds
((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Real; :: thesis: ( x in N implies ((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume A9: x in N ; :: thesis: ((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0))
reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;
thus ((- f1) . x) - ((- f1) . x0) = (- (f1 . x)) - ((- f1) . x0) by VALUED_1:8
.= (- (f1 . x)) - (- (f1 . x0)) by VALUED_1:8
.= - ((f1 . x) - (f1 . x0))
.= - ((L1 . (x - x0)) + (R1 . (x - x0))) by A4, A6, A9
.= (- (L1 . (x - x0))) + (- (R1 . (x - x0)))
.= (L . (xx - xx0)) + (- (R1 . (x - x0))) by A5, RFUNCT_1:58
.= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:58 ; :: thesis: verum

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; :: thesis: 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 ;
:: thesis: verum