let x0, r be Real; :: thesis: for n being Element of NAT st x0 in ].0 ,r.[ holds
(((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0))
let n be Element of NAT ; :: thesis: ( x0 in ].0 ,r.[ implies (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0)) )
assume A2: x0 in ].0 ,r.[ ; :: thesis: (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0))
A3: (#Z n) ^ is_differentiable_on ].0 ,r.[ by Th34;
A5: x0 <> 0 by A2, XXREAL_1:4;

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0))

then 0 < 0 + n ;
then n >= 1 by NAT_1:19;
then reconsider i = n - 1 as Element of NAT by INT_1:18;
x0 #Z i <> 0 by A5, PREPOWER:48;
then A8: x0 |^ i <> 0 by PREPOWER:46;
(((#Z n) ^ ) `| ].0 ,r.[) . x0 = diff ((#Z n) ^ ),x0 by A3, A2, FDIFF_1:def 8
.= - ((n * (x0 #Z i)) / ((x0 #Z n) ^2 )) by Th20, A5
.= - ((n * (x0 #Z i)) / ((x0 |^ n) ^2 )) by PREPOWER:46
.= - ((n * (x0 |^ i)) / ((x0 |^ n) ^2 )) by PREPOWER:46
.= - ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i)))) by NEWTON:13
.= - ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i)))
.= - ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i))) by NEWTON:13
.= - (n / (x0 |^ (i + 2))) by A8, XCMPLX_1:92
.= - (n / (x0 #Z (i + 2))) by PREPOWER:46
.= - (n / ((#Z (n + 1)) . x0)) by TAYLOR_1:def 1 ;
hence (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0)) ; :: thesis: verum

end;

suppose A9: n = 0 ; :: thesis: (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0))

(((#Z n) ^ ) `| ].0 ,r.[) . x0 = diff ((#Z n) ^ ),x0 by A3, A2, FDIFF_1:def 8
.= - ((0 * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 )) by A9, Th20, A5
.= - (n / ((#Z (n + 1)) . x0)) by A9 ;
hence (((#Z n) ^ ) `| ].0 ,r.[) . x0 = - (n / ((#Z (n + 1)) . x0)) ; :: thesis: verum

end;

end;