let a, b, c be Real; ( 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
; log (a,(b to_power c)) = c * (log (a,b))
A4:
b to_power c > 0
by A3, Th34;
a to_power (c * (log (a,b))) =
(a to_power (log (a,b))) to_power c
by A1, Th33
.=
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; verum