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:7, ZFMISC_1:34;
then A3: Z c= dom ((#Z (n + 1)) ^) by Th3;
A4: for x0 being Element of 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:7, ZFMISC_1:34;
then A5: Z c= dom ((#Z (n + 1)) ^) by Th3;
reconsider i = n - 1 as Element of NAT by A2, INT_1:5;
let x0 be Element of 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:38;
then A8: x0 |^ i <> 0 by PREPOWER:36;
(#Z n) ^ is_differentiable_on Z by A1, Th43;
then (((#Z n) ^) `| Z) . x0 = diff (((#Z n) ^),x0) by A7, FDIFF_1:def 7
.= - ((n * (x0 #Z (n - 1))) / ((x0 #Z n) ^2)) by A1, A7, Th29
.= - ((n * (x0 #Z i)) / ((x0 |^ n) ^2)) by PREPOWER:36
.= - ((n * (x0 |^ i)) / ((x0 |^ n) ^2)) by PREPOWER:36
.= - ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i)))) by NEWTON:8
.= - ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i)))
.= - ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i))) by NEWTON:8
.= - (n / (x0 |^ (i + 2))) by A8, XCMPLX_1:91
.= - (n / (x0 #Z (i + 2))) by PREPOWER:36
.= - (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 2
.= (- 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:49 ;
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 7;
dom (((- n) (#) ((#Z (n + 1)) ^)) | Z) = (dom ((- n) (#) ((#Z (n + 1)) ^))) /\ Z by RELAT_1:61
.= (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:5; :: thesis: verum