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

A3: log (number_e,d) in REAL by XREAL_0:def 1;
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:32, A3; :: thesis: verum

end;

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

end;

A4: dom (exp_R ") = right_open_halfline 0 by Th16, FUNCT_1:33;
then dom (exp_R ") = dom ln by Def2;
hence A5: ln = exp_R " by A4, A1, PARTFUN1:5; :: 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) ) )
A6: 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 A4, A5, Th17, FDIFF_1:9; :: thesis: verum

end;

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

end;

thus ln is one-to-one by A5, FUNCT_1:40; :: 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 A5, A6, A7, Th16, Th17, FUNCT_1:33; :: thesis: verum