theorem :: POWER:56

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