let a be positive non weightless Real; :: thesis: for b being positive Real holds
( log (a,b) = 0 iff b = 1 )
let b be positive Real; :: thesis: ( log (a,b) = 0 iff b = 1 )
A1: |.a.| <> 1 by TA1;
( log (a,b) = 0 implies b = 1 )

proof

a to_power (log (a,b)) = b ;
hence ( log (a,b) = 0 implies b = 1 ) by POWER:24; :: thesis: verum

end;

hence ( log (a,b) = 0 iff b = 1 ) by POWER:51, A1; :: thesis: verum