let Z be open Subset of REAL ; :: thesis:
let f, f1 be PartFunc of REAL , REAL ; :: thesis:
assume A1: ( Z c= dom (f ^ ) & f = ln * f1 & ( for x being Real st x in Z holds
( f1 . x = x & f1 . x > 0 ) ) & ( for x being Real st x in Z holds
f . x <> 0 ) ) ; :: thesis:
dom (f ^ ) c= dom f by RFUNCT_1:11;
then A2: Z c= dom f by A1, XBOOLE_1:1;
then A3: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 / x ) ) by A1, Th19;
then A4: f ^ is_differentiable_on Z by A1, FDIFF_2:22;
for x being Real st x in Z holds
((f ^ ) `| Z) . x = - (1 / (x * ((ln . x) ^2 )))

let x be Real; :: thesis:
assume A5: x in Z ; :: thesis:
then A6: ( f1 . x = x & f1 . x > 0 & f . x <> 0 ) by A1;
A7: f is_differentiable_in x by A3, A5, FDIFF_1:16;
((f ^ ) `| Z) . x = diff (f ^ ),x by A4, A5, FDIFF_1:def 8
.= - ((diff f,x) / ((f . x) ^2 )) by A6, A7, FDIFF_2:15
.= - (((f `| Z) . x) / ((f . x) ^2 )) by A3, A5, FDIFF_1:def 8
.= - ((1 / x) / (((ln * f1) . x) ^2 )) by A1, A2, A5, Th19
.= - ((1 / x) / ((ln . x) ^2 )) by A1, A2, A5, A6, FUNCT_1:22
.= - (1 / (x * ((ln . x) ^2 ))) by XCMPLX_1:79 ;
hence ((f ^ ) `| Z) . x = - (1 / (x * ((ln . x) ^2 ))) ; :: thesis:

end;

hence ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^ ) `| Z) . x = - (1 / (x * ((ln . x) ^2 ))) ) ) by A1, A3, FDIFF_2:22; :: thesis: