let Z be open Subset of REAL; :: thesis: ( not 0 in Z implies ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) )
set f = id Z;
A1: ( Z c= dom (id Z) & ( for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 ) ) by FUNCT_1:17;
then A2: id Z is_differentiable_on Z by FDIFF_1:23;
assume A3: not 0 in Z ; :: thesis: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) )
then A4: for x being Real st x in Z holds
(id Z) . x <> 0 by FUNCT_1:18;
then A5: (id Z) ^ is_differentiable_on Z by A2, FDIFF_2:22;

now :: thesis: for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2))

let x be Real; :: thesis: ( x in Z implies (((id Z) ^) `| Z) . x = - (1 / (x ^2)) )
assume A6: x in Z ; :: thesis: (((id Z) ^) `| Z) . x = - (1 / (x ^2))
then A7: ( (id Z) . x <> 0 & id Z is_differentiable_in x ) by A3, A2, FDIFF_1:9, FUNCT_1:18;
(((id Z) ^) `| Z) . x = diff (((id Z) ^),x) by A5, A6, FDIFF_1:def 7
.= - ((diff ((id Z),x)) / (((id Z) . x) ^2)) by A7, FDIFF_2:15
.= - ((((id Z) `| Z) . x) / (((id Z) . x) ^2)) by A2, A6, FDIFF_1:def 7
.= - (1 / (((id Z) . x) ^2)) by A1, A6, FDIFF_1:23
.= - (1 / (x ^2)) by A6, FUNCT_1:18 ;
hence (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ; :: thesis: verum

end;

hence ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by A2, A4, FDIFF_2:22; :: thesis: verum