let a be Real; :: thesis: ( a > 0 & a <> 1 implies log (a,a) = 1 )
assume A1: ( a > 0 & a <> 1 ) ; :: thesis: log (a,a) = 1
a to_power 1 = a ;
hence log (a,a) = 1 by A1, Def3; :: thesis: verum