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