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 that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 ; :: thesis: log a,(b to_power c) = c * (log a,b)
A4: b to_power c > 0 by A3, 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, A2, A3, Def3 ;
hence log a,(b to_power c) = c * (log a,b) by A1, A2, A4, Def3; :: thesis: verum