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