let a, b, c be real number ; :: thesis: ( a > 0 & a <> 1 & b > 0 implies log a,(b to_power c) = c * (log a,b) )
assume A1: ( a > 0 & a <> 1 & b > 0 ) ; :: thesis: log a,(b to_power c) = c * (log a,b)
then A2: b to_power c > 0 by Th39;
a to_power (c * (log a,b)) = (a to_power (log a,b)) to_power c by A1, Th38
.= b to_power c by A1, Def3 ;
hence log a,(b to_power c) = c * (log a,b) by A1, A2, Def3; :: thesis: verum