let a, b, c be Real; ( a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 implies log (a,c) = (log (a,b)) * (log (b,c)) )
assume that
A1:
a > 0
and
A2:
a <> 1
and
A3:
b > 0
and
A4:
b <> 1
and
A5:
c > 0
; log (a,c) = (log (a,b)) * (log (b,c))
a to_power ((log (a,b)) * (log (b,c))) =
(a to_power (log (a,b))) to_power (log (b,c))
by A1, Th33
.=
b to_power (log (b,c))
by A1, A2, A3, Def3
.=
c
by A3, A4, A5, Def3
;
hence
log (a,c) = (log (a,b)) * (log (b,c))
by A1, A2, A5, Def3; verum