|.a.| <> 1 by TA1;
hence a to_power (log (a,b)) = b by POWER:def 3; :: thesis: verum