theorem :: POLYEQ_4:23

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