let x, y be Element of 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:24
.= (exp_R x) * (exp (y * <i> )) by SIN_COS:54
.= (exp_R x) * ((cos y) + ((sin y) * <i> )) by SIN_COS:28 ;
hence exp (x + (y * <i> )) = (exp_R x) * ((cos y) + ((sin y) * <i> )) ; :: thesis: verum