theorem Th37: :: SIN_COS3:37

for z being Complex holds exp (- (<i> * z)) = (cos_C /. z) - (<i> * (sin_C /. z))