A1: for d being Element of REAL st d in right_open_halfline 0 holds
() . d = ln . d
proof
let d be Element of REAL ; :: thesis: ( d in right_open_halfline 0 implies () . d = ln . d )
assume A2: d in right_open_halfline 0 ; :: thesis: () . 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 ;
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 ; :: thesis: verum
end;
hence (exp_R ") . d = ln . d by ; :: thesis: verum
end;
A4: dom () = right_open_halfline 0 by ;
then dom () = dom ln by Def2;
hence A5: ln = exp_R " by ; :: 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:
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 ; :: 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 ; :: 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 ; :: thesis: verum