theorem Th18: :: SIN_COS3:18

for z being Complex holds cosh_C /. (<i> * z) = cos_C /. z