let x be Real; :: thesis: ( x <> 0 implies ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) ) )
set f = id REAL ;
assume A1: x <> 0 ; :: thesis: ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) )
( (id REAL ) . x = x #Z 1 & x #Z 1 = x |^ 1 ) by Lm2, PREPOWER:46, TAYLOR_1:def 1;
then A2: (id REAL ) . x <> 0 by A1, PREPOWER:12;
A3: id REAL is_differentiable_in x by Lm2, TAYLOR_1:2;
then diff ((id REAL ) ^ ),x = - ((diff (id REAL ),x) / (((id REAL ) . x) ^2 )) by A2, FDIFF_2:15
.= - ((1 * (x #Z (1 - 1))) / (((id REAL ) . x) ^2 )) by Lm2, TAYLOR_1:2
.= - ((1 * (x #Z 0 )) / (x ^2 )) by FUNCT_1:35
.= - (1 / (x ^2 )) by PREPOWER:44 ;
hence ( (id REAL ) ^ is_differentiable_in x & diff ((id REAL ) ^ ),x = - (1 / (x ^2 )) ) by A2, A3, FDIFF_2:15; :: thesis: verum