let
y
be
Real
;
:: thesis:
(
y
>
0
implies
exp_R
(
log
(
number_e
,
y
)
)
=
y
)
assume
y
>
0
;
:: thesis:
exp_R
(
log
(
number_e
,
y
)
)
=
y
then
number_e
to_power
(
log
(
number_e
,
y
)
)
=
y
by
Lm4
,
POWER:def 3
;
hence
exp_R
(
log
(
number_e
,
y
)
)
=
y
by
Th9
;
:: thesis:
verum