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

assume exp x = 1 ; :: thesis: x = 0

then exp_R x = 1 by SIN_COS:49;

hence x = 0 by EXpReq11; :: thesis: verum