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;
A2: for x being Real st x in Z holds
(id Z) . x = x by FUNCT_1:35;
AA: Z c= dom (id Z) by FUNCT_1:34;
X1: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
assume A1: 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 )) ) )
A4: ( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) ) by AA, X1, FDIFF_1:31;
A5: for x being Real st x in Z holds
(id Z) . x <> 0 by A1, FUNCT_1:35;
then A6: (id Z) ^ is_differentiable_on Z by A4, FDIFF_2:22;

now

let x be Real; :: thesis: ( x in Z implies (((id Z) ^ ) `| Z) . x = - (1 / (x ^2 )) )
assume A7: x in Z ; :: thesis: (((id Z) ^ ) `| Z) . x = - (1 / (x ^2 ))
then A8: (id Z) . x <> 0 by A2, A1;
A9: id Z is_differentiable_in x by A4, A7, FDIFF_1:16;
(((id Z) ^ ) `| Z) . x = diff ((id Z) ^ ),x by A6, A7, FDIFF_1:def 8
.= - ((diff (id Z),x) / (((id Z) . x) ^2 )) by A8, A9, FDIFF_2:15
.= - ((((id Z) `| Z) . x) / (((id Z) . x) ^2 )) by A4, A7, FDIFF_1:def 8
.= - (1 / (((id Z) . x) ^2 )) by A4, A7
.= - (1 / (x ^2 )) by A7, A2 ;
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 A4, A5, FDIFF_2:22; :: thesis: verum