let a, b, c be Real; :: thesis: ( a > 0 & a <> 1 & b > 0 & c > 0 implies (log (a,b)) + (log (a,c)) = log (a,(b * c)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 and
A4: c > 0 ; :: thesis: (log (a,b)) + (log (a,c)) = log (a,(b * c))
A5: a to_power ((log (a,b)) + (log (a,c))) = (a to_power (log (a,b))) * (a to_power (log (a,c))) by A1, Th27
.= b * (a to_power (log (a,c))) by A1, A2, A3, Def3
.= b * c by A1, A2, A4, Def3 ;
b * c > 0 by A3, A4, XREAL_1:129;
hence (log (a,b)) + (log (a,c)) = log (a,(b * c)) by A1, A2, A5, Def3; :: thesis: verum