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

proof

assume log (a,b) = 1 ; :: thesis: a = b
then b = a to_power 1 ;
hence a = b ; :: thesis: verum

end;

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