let a be Real; :: thesis:
let Z be open Subset of REAL ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
assume A1: ( Z c= dom (ln * f) & ( for x being Real st x in Z holds
( f . x = x - a & f . x > 0 ) ) ) ; :: thesis:
then for y being set st y in Z holds
y in dom f by FUNCT_1:21;
then A2: Z c= dom f by TARSKI:def 3;
A3: for x being Real st x in Z holds
f . x = (1 * x) + (- a)

let x be Real; :: thesis:
assume A4: x in Z ; :: thesis:
(1 * x) + (- a) = (1 * x) - a ;
hence f . x = (1 * x) + (- a) by A1, A4; :: thesis:

end;

then A5: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) ) by A2, FDIFF_1:31;
A6: for x being Real st x in Z holds
ln * f is_differentiable_in x

let x be Real; :: thesis:
assume A7: x in Z ; :: thesis:
then A8: f is_differentiable_in x by A5, FDIFF_1:16;
f . x > 0 by A1, A7;
hence ln * f is_differentiable_in x by A8, TAYLOR_1:20; :: thesis:

end;

then A9: ln * f is_differentiable_on Z by A1, FDIFF_1:16;
for x being Real st x in Z holds
((ln * f) `| Z) . x = 1 / (x - a)

let x be Real; :: thesis:
assume A10: x in Z ; :: thesis:
then A11: f is_differentiable_in x by A5, FDIFF_1:16;
A12: ( f . x = x - a & f . x > 0 ) by A1, A10;
then diff (ln * f),x = (diff f,x) / (f . x) by A11, TAYLOR_1:20
.= ((f `| Z) . x) / (f . x) by A5, A10, FDIFF_1:def 8
.= 1 / (x - a) by A2, A3, A10, A12, FDIFF_1:31 ;
hence ((ln * f) `| Z) . x = 1 / (x - a) by A9, A10, FDIFF_1:def 8; :: thesis:

end;

hence ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * f) `| Z) . x = 1 / (x - a) ) ) by A1, A6, FDIFF_1:16; :: thesis: