let r be Real; :: thesis:
assume A2: ].0 ,r.[ c= dom ((#Z 3) ^ ) ; :: thesis:
(#Z 2) ^ is_differentiable_on ].0 ,r.[ by Th34;
then A4: dom (((#Z 2) ^ ) `| ].0 ,r.[) = ].0 ,r.[ by FDIFF_1:def 8;
A5: dom (((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[) = (dom ((- 2) (#) ((#Z 3) ^ ))) /\ ].0 ,r.[ by FUNCT_1:68
.= (dom ((#Z 3) ^ )) /\ ].0 ,r.[ by VALUED_1:def 5
.= ].0 ,r.[ by A2, XBOOLE_1:28 ;
for x0 being Real st x0 in ].0 ,r.[ holds
(((#Z 2) ^ ) `| ].0 ,r.[) . x0 = (((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[) . x0

proof

let x0 be Real; :: thesis:
assume A8: x0 in ].0 ,r.[ ; :: thesis:
A9: (#Z 2) ^ is_differentiable_on ].0 ,r.[ by Th34;
A11: x0 <> 0 by A8, XXREAL_1:4;
A13: dom ((- 2) (#) ((#Z 3) ^ )) = dom ((#Z 3) ^ ) by VALUED_1:def 5;
reconsider i = 2 - 1 as Element of NAT ;
A16: x0 #Z i <> 0 by A11, PREPOWER:48;
A17: x0 |^ i <> 0 by A16, PREPOWER:46;
(((#Z 2) ^ ) `| ].0 ,r.[) . x0 = diff ((#Z 2) ^ ),x0 by A9, A8, FDIFF_1:def 8
.= - ((2 * (x0 #Z 1)) / ((x0 #Z 2) ^2 )) by ThB, A11
.= - ((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 A17, 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 A8, A2, RFUNCT_1:def 8
.= (- 2) * (((#Z 3) ^ ) . x0)
.= ((- 2) (#) ((#Z 3) ^ )) . x0 by A8, A2, A13, VALUED_1:def 5
.= (((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[) . x0 by A8, FUNCT_1:72 ;
hence (((#Z 2) ^ ) `| ].0 ,r.[) . x0 = (((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[) . x0 ; :: thesis:

end;

hence ((#Z 2) ^ ) `| ].0 ,r.[ = ((- 2) (#) ((#Z 3) ^ )) | ].0 ,r.[ by A5, A4, PARTFUN1:34; :: thesis: