theorem Th30: :: SIN_COS7:30

for x being Real st 0 <> x holds
((exp_R x) ^2) - 1 <> 0