let
a
,
x
be
Real
;
:: thesis:
(
a
>
0
&
a
<>
1 &
a
to_power
x
=
a
implies
x
=
1 )
assume
that
A1
: (
a
>
0
&
a
<>
1 )
and
A2
:
a
to_power
x
=
a
;
:: thesis:
x
=
1
x
=
log
(
a
,
a
)
by
A1
,
A2
,
POWER:def 3
;
hence
x
=
1
by
A1
,
POWER:52
;
:: thesis:
verum