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 that

A1: Z c= dom (- (ln * f)) and

A2: 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 for y being object st y in Z holds

y in dom f by FUNCT_1:11;

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

A8: for x being Real st x in Z holds

((- (ln * f)) `| Z) . x = 1 / (a - x)

hence ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) by A7, A8, FDIFF_1:20; :: thesis: verum

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 that

A1: Z c= dom (- (ln * f)) and

A2: 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) ) )

now :: thesis: for y being object st y in Z holds

y in dom (ln * f)

then A3:
Z c= dom (ln * f)
by TARSKI:def 3;y in dom (ln * f)

let y be object ; :: 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;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

then for y being object st y in Z holds

y in dom f by FUNCT_1:11;

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

then A6:
f is_differentiable_on Z
by A4, FDIFF_1:23;
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 A2;

hence f . x = ((- 1) * x) + a ; :: thesis: verum

end;assume x in Z ; :: thesis: f . x = ((- 1) * x) + a

then f . x = a - x by A2;

hence f . x = ((- 1) * x) + a ; :: thesis: verum

now :: thesis: for x being Real st x in Z holds

ln * f is_differentiable_in x

then A7:
ln * f is_differentiable_on Z
by A3, FDIFF_1:9;ln * f is_differentiable_in x

let x be Real; :: thesis: ( x in Z implies ln * f is_differentiable_in x )

assume x in Z ; :: thesis: ln * f is_differentiable_in x

then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9;

hence ln * f is_differentiable_in x by TAYLOR_1:20; :: thesis: verum

end;assume x in Z ; :: thesis: ln * f is_differentiable_in x

then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9;

hence ln * f is_differentiable_in x by TAYLOR_1:20; :: thesis: verum

A8: for x being Real st x in Z holds

((- (ln * f)) `| Z) . x = 1 / (a - x)

proof

Z c= dom ((- 1) (#) (ln * f))
by A1;
let x be Real; :: thesis: ( x in Z implies ((- (ln * f)) `| Z) . x = 1 / (a - x) )

assume A9: x in Z ; :: thesis: ((- (ln * f)) `| Z) . x = 1 / (a - x)

then A10: f . x = a - x by A2;

( f . x > 0 & f is_differentiable_in x ) by A2, A6, A9, FDIFF_1:9;

then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20

.= ((f `| Z) . x) / (f . x) by A6, A9, FDIFF_1:def 7

.= (- 1) / (a - x) by A4, A5, A9, A10, FDIFF_1:23 ;

then (((- 1) (#) (ln * f)) `| Z) . x = (- 1) * ((- 1) / (a - x)) by A1, A7, A9, FDIFF_1:20

.= ((- 1) * (- 1)) / (a - x) by XCMPLX_1:74

.= 1 / (a - x) ;

hence ((- (ln * f)) `| Z) . x = 1 / (a - x) ; :: thesis: verum

end;assume A9: x in Z ; :: thesis: ((- (ln * f)) `| Z) . x = 1 / (a - x)

then A10: f . x = a - x by A2;

( f . x > 0 & f is_differentiable_in x ) by A2, A6, A9, FDIFF_1:9;

then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20

.= ((f `| Z) . x) / (f . x) by A6, A9, FDIFF_1:def 7

.= (- 1) / (a - x) by A4, A5, A9, A10, FDIFF_1:23 ;

then (((- 1) (#) (ln * f)) `| Z) . x = (- 1) * ((- 1) / (a - x)) by A1, A7, A9, FDIFF_1:20

.= ((- 1) * (- 1)) / (a - x) by XCMPLX_1:74

.= 1 / (a - x) ;

hence ((- (ln * f)) `| Z) . x = 1 / (a - x) ; :: thesis: verum

hence ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) by A7, A8, FDIFF_1:20; :: thesis: verum