let x be Real; :: thesis: ( 0 <> x implies ((exp_R x) ^2) - 1 <> 0 )
assume A1: 0 <> x ; :: thesis: ((exp_R x) ^2) - 1 <> 0
assume ((exp_R x) ^2) - 1 = 0 ; :: thesis: contradiction
then ( exp_R x = 1 or exp_R x = - 1 ) by XCMPLX_1:182;
hence contradiction by A1, Th29, SIN_COS:55; :: thesis: verum