A1: dom (exp_R " ) = right_open_halfline 0 by Th16, FUNCT_1:55;
then A2: dom (exp_R " ) = dom ln by Def2;
for d being Element of REAL st d in right_open_halfline 0 holds
(exp_R " ) . d = ln . d

proof

let d be Element of REAL ; :: thesis: ( d in right_open_halfline 0 implies (exp_R " ) . d = ln . d )
assume A3: d in right_open_halfline 0 ; :: thesis: (exp_R " ) . d = ln . d
(exp_R " ) . d = log number_e ,d

proof

d in { g where g is Real : 0 < g } by A3, XXREAL_1:230;
then consider g being Real such that
A4: ( g = d & g > 0 ) ;
d = exp_R . (log number_e ,d) by A4, Th15;
hence (exp_R " ) . d = log number_e ,d by Th16, FUNCT_1:54; :: thesis: verum

end;

hence (exp_R " ) . d = ln . d by A3, Def2; :: thesis: verum

end;

hence A5: ln = exp_R " by A1, A2, PARTFUN1:34; :: thesis: ( ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff ln ,x = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff ln ,x ) )
hence ln is one-to-one by FUNCT_1:62; :: thesis: ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff ln ,x = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff ln ,x ) )
A6: dom ln = right_open_halfline 0 by Def2;
A7: for x being Real st x > 0 holds
ln is_differentiable_in x

proof

let x be Real; :: thesis: ( x > 0 implies ln is_differentiable_in x )
assume A8: x > 0 ; :: thesis: ln is_differentiable_in x
A9: x in right_open_halfline 0

proof

x in { g where g is Real : 0 < g } by A8;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum

end;

thus ln is_differentiable_in x by A1, A5, A9, Th17, FDIFF_1:16; :: thesis: verum

end;

for x being Element of right_open_halfline 0 holds 0 < diff ln ,x

proof

let x be Element of right_open_halfline 0 ; :: thesis: 0 < diff ln ,x
x in right_open_halfline 0 ;
then x in { g where g is Real : 0 < g } by XXREAL_1:230;
then consider g being Real such that
A10: ( x = g & 0 < g ) ;
A11: x " > 0 by A10;
1 / x = x " by XCMPLX_1:217;
hence 0 < diff ln ,x by A1, A5, A11, Th17; :: thesis: verum

end;

hence ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff ln ,x = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff ln ,x ) ) by A5, A6, A7, Th16, Th17, FUNCT_1:55; :: thesis: verum