let a, b be positive non weightless Real; :: thesis: log (a,b) = 1 / (log (b,a))
A1: ( a > 0 & b > 0 & a <> 1 & b <> 1 ) by TA1;
( a to_power (log (a,b)) = b & b to_power (log (b,a)) = a ) ;
then a = a to_power ((log (a,b)) * (log (b,a))) by POWER:33;
then (log (a,b)) * (log (b,a)) = log (a,a)
.= 1 by A1, POWER:52 ;
hence log (a,b) = 1 / (log (b,a)) by XCMPLX_1:73; :: thesis: verum