let
x
be
Real
;
:: thesis:
log
(
number_e
,
(
exp_R
.
x
)
)
=
x
thus
log
(
number_e
,
(
exp_R
.
x
)
) =
log
(
number_e
,
(
exp_R
x
)
)
by
SIN_COS:def 23
.=
x
by
Th12
;
:: thesis:
verum