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