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