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
A2: a to_power 1 = a by Th30;
thus log a,a = 1 by A1, A2, Def3; :: thesis: verum