theorem :: POWER:54

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))