let x, y be Real; :: thesis: exp (x + (y * <i>)) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i>)
exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>)) by Lm4
.= (((exp_R x) * (cos y)) - (0 * (sin y))) + ((((exp_R x) * (sin y)) + ((cos y) * 0)) * <i>)
.= ((exp_R x) * (cos . y)) + (((exp_R x) * (sin y)) * <i>) by SIN_COS:def 19
.= ((exp_R . x) * (cos . y)) + (((exp_R x) * (sin y)) * <i>) by SIN_COS:def 23
.= ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin y)) * <i>) by SIN_COS:def 23 ;
hence exp (x + (y * <i>)) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i>) by SIN_COS:def 17; :: thesis: verum