let
y
be
Real
;
:: thesis:
(
y
>
0
implies
exp_R
.
(
log
(
number_e
,
y
)
)
=
y
)
assume
A1
:
y
>
0
;
:: thesis:
exp_R
.
(
log
(
number_e
,
y
)
)
=
y
thus
exp_R
.
(
log
(
number_e
,
y
)
)
=
exp_R
(
log
(
number_e
,
y
)
)
by
SIN_COS:def 23
.=
y
by
A1
,
Th14
;
:: thesis:
verum