let r be Real; :: thesis: for n being Element of NAT st n >= 1 holds
((#Z n) ^ ) `| ].0 ,r.[ = ((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[
let n be Element of NAT ; :: thesis: ( n >= 1 implies ((#Z n) ^ ) `| ].0 ,r.[ = ((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[ )
assume A1: n >= 1 ; :: thesis: ((#Z n) ^ ) `| ].0 ,r.[ = ((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[
A3: n + 1 >= 1 + 0 by XREAL_1:9;
].0 ,r.[ c= REAL \ {0 } by Lm2;
then A4: ].0 ,r.[ c= dom ((#Z (n + 1)) ^ ) by Th36, A3;
(#Z n) ^ is_differentiable_on ].0 ,r.[ by Th34;
then A5: dom (((#Z n) ^ ) `| ].0 ,r.[) = ].0 ,r.[ by FDIFF_1:def 8;
A6: dom (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) = (dom ((- n) (#) ((#Z (n + 1)) ^ ))) /\ ].0 ,r.[ by FUNCT_1:68
.= (dom ((#Z (n + 1)) ^ )) /\ ].0 ,r.[ by VALUED_1:def 5
.= ].0 ,r.[ by A4, XBOOLE_1:28 ;
for x0 being Real st x0 in ].0 ,r.[ holds
(((#Z n) ^ ) `| ].0 ,r.[) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) . x0

proof

let x0 be Real; :: thesis: ( x0 in ].0 ,r.[ implies (((#Z n) ^ ) `| ].0 ,r.[) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) . x0 )
assume A9: x0 in ].0 ,r.[ ; :: thesis: (((#Z n) ^ ) `| ].0 ,r.[) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) . x0
A10: (#Z n) ^ is_differentiable_on ].0 ,r.[ by Th34;
A12: x0 <> 0 by A9, XXREAL_1:4;
A14: dom ((- n) (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ ) by VALUED_1:def 5;
A15: n + 1 >= 1 + 0 by XREAL_1:9;
].0 ,r.[ c= REAL \ {0 } by Lm2;
then A17: ].0 ,r.[ c= dom ((#Z (n + 1)) ^ ) by Th36, A15;
reconsider i = n - 1 as Element of NAT by A1, INT_1:18;
A18: x0 #Z i <> 0 by A12, PREPOWER:48;
A19: x0 |^ i <> 0 by A18, PREPOWER:46;
(((#Z n) ^ ) `| ].0 ,r.[) . x0 = diff ((#Z n) ^ ),x0 by A10, A9, FDIFF_1:def 8
.= - ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 )) by Th20, A12
.= - ((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 A19, XCMPLX_1:92
.= - (n / (x0 #Z (i + 2))) by PREPOWER:46
.= - (n / ((#Z (i + 2)) . x0)) by TAYLOR_1:def 1
.= - (n * (((#Z (n + 1)) . x0) " )) by XCMPLX_0:def 9
.= - (n * (((#Z (n + 1)) ^ ) . x0)) by A9, A17, RFUNCT_1:def 8
.= (- n) * (((#Z (n + 1)) ^ ) . x0)
.= ((- n) (#) ((#Z (n + 1)) ^ )) . x0 by A9, A14, A17, VALUED_1:def 5
.= (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) . x0 by A9, FUNCT_1:72 ;
hence (((#Z n) ^ ) `| ].0 ,r.[) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[) . x0 ; :: thesis: verum

end;

hence ((#Z n) ^ ) `| ].0 ,r.[ = ((- n) (#) ((#Z (n + 1)) ^ )) | ].0 ,r.[ by A5, A6, PARTFUN1:34; :: thesis: verum