let x, y be Real; :: thesis: exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>))
exp (x + (y * <i>)) = (exp x) * (exp (y * <i>)) by SIN_COS:23
.= (exp_R x) * (exp (y * <i>)) by SIN_COS:49
.= (exp_R x) * ((cos y) + ((sin y) * <i>)) by SIN_COS:25 ;
hence exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>)) ; :: thesis: verum