for a, x being Real st a > 0 & a <> 1 & a to_power x = 1 holds
x = 0