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 by POWER:30; :: thesis: verum