A1: 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 A2: 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 A2, XXREAL_1:230;
then ex g being Real st
( g = d & g > 0 ) ;
then d = exp_R . (log number_e ,d) by Th15;
hence (exp_R " ) . d = log number_e ,d by Th16, FUNCT_1:54; :: thesis: verum

end;

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

end;

A3: dom (exp_R " ) = right_open_halfline 0 by Th16, FUNCT_1:55;
then dom (exp_R " ) = dom ln by Def2;
hence A4: ln = exp_R " by A3, A1, 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 ) )
A5: 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 x > 0 ; :: thesis: ln is_differentiable_in x
then x in { g where g is Real : 0 < g } ;
then x in right_open_halfline 0 by XXREAL_1:230;
hence ln is_differentiable_in x by A3, A4, Th17, FDIFF_1:16; :: thesis: verum

end;

A6: 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 A7: ex g being Real st
( x = g & 0 < g ) ;
1 / x = x " by XCMPLX_1:217;
hence 0 < diff ln ,x by A3, A4, A7, Th17; :: thesis: verum

end;

thus ln is one-to-one by A4, 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 ) )
dom ln = right_open_halfline 0 by Def2;
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 A4, A5, A6, Th16, Th17, FUNCT_1:55; :: thesis: verum