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