theorem :: POWER:55

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