let Z be open Subset of REAL ; :: thesis:
set f = ln ;
assume A1: Z c= dom ((id Z) (#) ln ) ; :: thesis:
then Z c= (dom (id Z)) /\ (dom ln ) by VALUED_1:def 4;
then A2: ( Z c= dom (id Z) & Z c= dom ln ) by XBOOLE_1:18;
A3: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
then A4: ( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) ) by A2, FDIFF_1:31;
A5: ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) ) by A2, Th19;
for x being Real st x in Z holds
(((id Z) (#) ln ) `| Z) . x = 1 + (ln . x)

proof

let x be Real; :: thesis:
assume A6: x in Z ; :: thesis:
then A7: x <> 0 by Lem10, A2;
(((id Z) (#) ln ) `| Z) . x = (((id Z) . x) * (diff ln ,x)) + ((ln . x) * (diff (id Z),x)) by A1, A4, A5, A6, FDIFF_1:29
.= (((id Z) . x) * ((ln `| Z) . x)) + ((ln . x) * (diff (id Z),x)) by A5, A6, FDIFF_1:def 8
.= (((id Z) . x) * (1 / x)) + ((ln . x) * (diff (id Z),x)) by A2, A6, Th19
.= (x * (1 / x)) + ((ln . x) * (diff (id Z),x)) by A6, FUNCT_1:35
.= (x * (1 / x)) + ((ln . x) * (((id Z) `| Z) . x)) by A4, A6, FDIFF_1:def 8
.= (x * (1 / x)) + ((ln . x) * 1) by A2, A3, A6, FDIFF_1:31
.= 1 + (ln . x) by A7, XCMPLX_1:107 ;
hence (((id Z) (#) ln ) `| Z) . x = 1 + (ln . x) ; :: thesis:

end;

hence ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ln ) `| Z) . x = 1 + (ln . x) ) ) by A1, A4, A5, FDIFF_1:29; :: thesis: