theorem Th19: :: SIN_COS3:19

for x, y being Real holds exp (x + (y * <i>)) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i>)