let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st not 0 in Z & n >= 1 holds
((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z
let Z be open Subset of REAL ; :: thesis: ( not 0 in Z & n >= 1 implies ((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z )
assume that
A1: not 0 in Z and
A2: n >= 1 ; :: thesis: ((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z
( n + 1 >= 1 + 0 & Z c= REAL \ {0 } ) by A1, XREAL_1:9, ZFMISC_1:40;
then A3: Z c= dom ((#Z (n + 1)) ^ ) by Th3;
A4: for x0 being Real st x0 in Z holds
(((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0

proof

( n + 1 >= 1 + 0 & Z c= REAL \ {0 } ) by A1, XREAL_1:9, ZFMISC_1:40;
then A5: Z c= dom ((#Z (n + 1)) ^ ) by Th3;
reconsider i = n - 1 as Element of NAT by A2, INT_1:18;
let x0 be Real; :: thesis: ( x0 in Z implies (((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0 )
A6: dom ((- n) (#) ((#Z (n + 1)) ^ )) = dom ((#Z (n + 1)) ^ ) by VALUED_1:def 5;
assume A7: x0 in Z ; :: thesis: (((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0
then x0 #Z i <> 0 by A1, PREPOWER:48;
then A8: x0 |^ i <> 0 by PREPOWER:46;
(#Z n) ^ is_differentiable_on Z by A1, Th43;
then (((#Z n) ^ ) `| Z) . x0 = diff ((#Z n) ^ ),x0 by A7, FDIFF_1:def 8
.= - ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2 )) by A1, A7, Th29
.= - ((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 (i + 2)) . x0)) by TAYLOR_1:def 1
.= - (n * (((#Z (n + 1)) . x0) " )) by XCMPLX_0:def 9
.= - (n * (((#Z (n + 1)) ^ ) . x0)) by A7, A5, RFUNCT_1:def 8
.= (- n) * (((#Z (n + 1)) ^ ) . x0)
.= ((- n) (#) ((#Z (n + 1)) ^ )) . x0 by A7, A6, A5, VALUED_1:def 5
.= (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0 by A7, FUNCT_1:72 ;
hence (((#Z n) ^ ) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^ )) | Z) . x0 ; :: thesis: verum

end;

(#Z n) ^ is_differentiable_on Z by A1, Th43;
then A9: dom (((#Z n) ^ ) `| Z) = Z by FDIFF_1:def 8;
dom (((- n) (#) ((#Z (n + 1)) ^ )) | Z) = (dom ((- n) (#) ((#Z (n + 1)) ^ ))) /\ Z by RELAT_1:90
.= (dom ((#Z (n + 1)) ^ )) /\ Z by VALUED_1:def 5
.= Z by A3, XBOOLE_1:28 ;
hence ((#Z n) ^ ) `| Z = ((- n) (#) ((#Z (n + 1)) ^ )) | Z by A9, A4, PARTFUN1:34; :: thesis: verum