let x be Real; :: 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, Lm1, POWER:51, TAYLOR_1:11 ;
hence contradiction by A1; :: thesis: verum