theorem Th36: :: SIN_COS3:36
for z being Complex holds exp (<i> * z) = (cos_C /. z) + (<i> * (sin_C /. z))