let Z be open Subset of REAL ; :: thesis: ( not 0 in Z implies ((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z )
assume A1: not 0 in Z ; :: thesis: ((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z
then (#Z 2) ^ is_differentiable_on Z by Th43;
then A2: dom (((#Z 2) ^ ) `| Z) = Z by FDIFF_1:def 8;
Z c= REAL \ {0 } by A1, ZFMISC_1:40;
then A3: Z c= dom ((#Z 3) ^ ) by Th3;
A4: for x0 being Real st x0 in Z holds
(((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0

proof

reconsider i = 2 - 1 as Element of NAT ;
let x0 be Real; :: thesis: ( x0 in Z implies (((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0 )
A5: dom ((- 2) (#) ((#Z 3) ^ )) = dom ((#Z 3) ^ ) by VALUED_1:def 5;
assume A6: x0 in Z ; :: thesis: (((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0
then x0 #Z i <> 0 by A1, PREPOWER:48;
then A7: x0 |^ i <> 0 by PREPOWER:46;
(#Z 2) ^ is_differentiable_on Z by A1, Th43;
then (((#Z 2) ^ ) `| Z) . x0 = diff ((#Z 2) ^ ),x0 by A6, FDIFF_1:def 8
.= - ((2 * x0) / ((x0 #Z 2) ^2 )) by A1, A6, Th47
.= - ((2 * (x0 #Z 1)) / ((x0 #Z 2) ^2 )) by PREPOWER:45
.= - ((2 * (x0 #Z 1)) / ((x0 |^ 2) ^2 )) by PREPOWER:46
.= - ((2 * (x0 |^ 1)) / ((x0 |^ 2) * (x0 |^ (1 + 1)))) by PREPOWER:46
.= - ((2 * (x0 |^ 1)) / ((x0 |^ 2) * ((x0 |^ 1) * (x0 |^ 1)))) by NEWTON:13
.= - ((2 * (x0 |^ 1)) / (((x0 |^ 2) * (x0 |^ 1)) * (x0 |^ 1)))
.= - ((2 * (x0 |^ 1)) / ((x0 |^ (2 + 1)) * (x0 |^ 1))) by NEWTON:13
.= - (2 / (x0 |^ (1 + 2))) by A7, XCMPLX_1:92
.= - (2 / (x0 #Z 3)) by PREPOWER:46
.= - (2 / ((#Z 3) . x0)) by TAYLOR_1:def 1
.= - (2 * (((#Z 3) . x0) " )) by XCMPLX_0:def 9
.= - (2 * (((#Z 3) ^ ) . x0)) by A3, A6, RFUNCT_1:def 8
.= (- 2) * (((#Z 3) ^ ) . x0)
.= ((- 2) (#) ((#Z 3) ^ )) . x0 by A3, A6, A5, VALUED_1:def 5
.= (((- 2) (#) ((#Z 3) ^ )) | Z) . x0 by A6, FUNCT_1:72 ;
hence (((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0 ; :: thesis: verum

end;

dom (((- 2) (#) ((#Z 3) ^ )) | Z) = (dom ((- 2) (#) ((#Z 3) ^ ))) /\ Z by RELAT_1:90
.= (dom ((#Z 3) ^ )) /\ Z by VALUED_1:def 5
.= Z by A3, XBOOLE_1:28 ;
hence ((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z by A2, A4, PARTFUN1:34; :: thesis: verum