let a be real number ; :: 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 by Th30;
hence log a,a = 1 by A1, Def3; :: thesis: verum