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 A1: ( a > 0 & a <> 1 & b >= 0 & 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 A1;

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, POWER:61
.= ((b * c) * (log a,b)) + ((b * c) * (log a,c)) ;
:: thesis: verum

end;

end;