let a, b, c be Real; :: thesis: ( a > 0 & c > 0 & c <> 1 implies a to_power b = c to_power (b * (log (c,a))) )
assume that
A1: a > 0 and
A2: c > 0 and
A3: c <> 1 ; :: thesis: a to_power b = c to_power (b * (log (c,a)))
A4: a to_power b > 0 by A1, POWER:34;
log (c,(a to_power b)) = b * (log (c,a)) by A1, A2, A3, POWER:55;
hence a to_power b = c to_power (b * (log (c,a))) by A2, A3, A4, POWER:def 3; :: thesis: verum