let f1 be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL st Z c= dom (- f1) & f1 is_differentiable_on Z holds
( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x)) ) )
let Z be open Subset of REAL; :: thesis: ( Z c= dom (- f1) & f1 is_differentiable_on Z implies ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x)) ) ) )
assume that
A1: Z c= dom (- f1) and
A2: f1 is_differentiable_on Z ; :: thesis: ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x)) ) )

now :: thesis: for x0 being Real st x0 in Z holds
- f1 is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies - f1 is_differentiable_in x0 )
assume x0 in Z ; :: thesis: - f1 is_differentiable_in x0
then f1 is_differentiable_in x0 by A2, FDIFF_1:9;
hence - f1 is_differentiable_in x0 by Th22; :: thesis: verum

end;

hence A3: - f1 is_differentiable_on Z by A1, FDIFF_1:9; :: thesis: for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x))

now :: thesis: for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x))

let x be Real; :: thesis: ( x in Z implies ((- f1) `| Z) . x = - (diff (f1,x)) )
assume A4: x in Z ; :: thesis: ((- f1) `| Z) . x = - (diff (f1,x))
then A5: f1 is_differentiable_in x by A2, FDIFF_1:9;
thus ((- f1) `| Z) . x = diff ((- f1),x) by A3, A4, FDIFF_1:def 7
.= - (diff (f1,x)) by A5, Th22 ; :: thesis: verum

end;

hence for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x)) ; :: thesis: verum