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