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