for a, b, c being Real st a > 0 & c > 0 & c <> 1 holds
a to_power b = c to_power (b * (log (c,a))) by Lm3;