let x be Real; :: thesis: ( exp x = 1 implies x = 0 )
assume exp x = 1 ; :: thesis: x = 0
then exp_R x = 1 by SIN_COS:49;
hence x = 0 by EXpReq11; :: thesis: verum