let x be real number ; :: thesis: ( x <> 0 implies exp_R x <> 1 )
assume A1: x <> 0 ; :: thesis: exp_R x <> 1
assume A2: exp_R x = 1 ; :: thesis: contradiction
x = log number_e ,(exp_R x) by TAYLOR_1:12
.= 0 by A2, Lm2, POWER:59 ;
hence contradiction by A1; :: thesis: verum