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