let a, b, c be Real; :: thesis: ( a > 0 & a <> 1 & b >= 0 & c >= 0 implies (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b >= 0 and
A4: c >= 0 ; :: thesis: (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c))

per cases ( ( b > 0 & c = 0 ) or ( b = 0 & c = 0 ) or ( b = 0 & c > 0 ) or ( b > 0 & c > 0 ) ) by A3, A4;

suppose ( b > 0 & c = 0 ) ; :: thesis: (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c))

hence (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c)) ; :: thesis: verum

end;

suppose ( b = 0 & c = 0 ) ; :: thesis: (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c))

hence (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c)) ; :: thesis: verum

end;

suppose ( b = 0 & c > 0 ) ; :: thesis: (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c))

hence (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c)) ; :: thesis: verum

end;

suppose ( b > 0 & c > 0 ) ; :: thesis: (b * c) * (log a,(b * c)) = ((b * c) * (log a,b)) + ((b * c) * (log a,c))

hence (b * c) * (log a,(b * c)) = (b * c) * ((log a,b) + (log a,c)) by A1, A2, POWER:61
.= ((b * c) * (log a,b)) + ((b * c) * (log a,c)) ;
:: thesis: verum

end;

end;