A1:
for d being Element of REAL st d in right_open_halfline 0 holds

(exp_R ") . d = ln . d

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

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

(exp_R ") . d = ln . d

proof

A4:
dom (exp_R ") = right_open_halfline 0
by Th16, FUNCT_1:33;
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)

end;assume A2: d in right_open_halfline 0 ; :: thesis: (exp_R ") . d = ln . d

(exp_R ") . d = log (number_e,d)

proof

hence
(exp_R ") . d = ln . d
by A2, Def2; :: thesis: verum
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;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

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

A7:
for x being Element of right_open_halfline 0 holds 0 < diff (ln,x)
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;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

proof

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
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;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

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