theorem :: POWER:53

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