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 LINEAR ex R being REST st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by FDIFF_1:def 5;
consider L1 being LINEAR, R1 being REST 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 REST by Th21;
reconsider L = - L1 as LINEAR by Th20;
A5: L1 is total by FDIFF_1:def 4;
consider N being Neighbourhood of x0 such that
A6: N c= N1 ;
A7: R1 is total by FDIFF_1:def 3;

A8: now

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))
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 . (x - x0)) + (- (R1 . (x - x0))) by A5, RFUNCT_1:74
.= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:74 ; :: 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 5; :: thesis: diff (- f1),x0 = - (diff f1,x0)
hence diff (- f1),x0 = L . 1 by A10, A8, FDIFF_1:def 6
.= - (L1 . 1) by A5, RFUNCT_1:74
.= - (diff f1,x0) by A1, A2, A4, FDIFF_1:def 6 ;
:: thesis: verum