for x being Real st x <> 0 holds
exp_R x <> 1