let a be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) implies ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) )
assume A1: ( Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) ) ; :: thesis: ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * f)) `| Z) . x = 1 / (a - x) ) )
then A2: ( Z c= dom ((- 1) (#) (ln * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) ) ;

now

let y be set ; :: thesis: ( y in Z implies y in dom (ln * f) )
assume y in Z ; :: thesis: y in dom (ln * f)
then y in dom ((- 1) (#) (ln * f)) by A1;
hence y in dom (ln * f) by VALUED_1:def 5; :: thesis: verum

end;

then A3: Z c= dom (ln * f) by TARSKI:def 3;
then for y being set st y in Z holds
y in dom f by FUNCT_1:21;
then A4: Z c= dom f by TARSKI:def 3;
A5: for x being Real st x in Z holds
f . x = ((- 1) * x) + a

proof

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

end;

then A6: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = - 1 ) ) by A4, FDIFF_1:31;

now

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

end;

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

proof

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

end;

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