let
x
be
Real
;
:: thesis:
log
(
number_e
,
(
exp_R
x
)
)
=
x
(
exp_R
x
>
0
&
number_e
to_power
x
=
exp_R
x
)
by
Th9
,
SIN_COS:55
;
hence
log
(
number_e
,
(
exp_R
x
)
)
=
x
by
Lm4
,
POWER:def 3
;
:: thesis:
verum