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:39;
log c,(a to_power b) = b * (log c,a) by A1, A2, A3, POWER:63;
hence a to_power b = c to_power (b * (log c,a)) by A2, A3, A4, POWER:def 3; :: thesis: verum