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