Show that $X_t = (cos(W_t) , sin(W_t))$ solves the SDE system:
$$dX^1 = - \frac{1}{2}X^1dt - X^2dW_t$$ $$dX^2 = - \frac{1}{2}X^2dt + X^1dW_t$$
Show also that if $X = (X^1,X^2)$ is any other solution, then $\lvert X \rvert$ is constant in time.
Showing the first part follows from a straightforward application of Ito's formula. My question pertains to the second. This is from Lawrence Evans, Intro to Stochastic Differential Equations.
I've unsuccessfully tinkered for some time using the integral forms of $dX^1$ and $dX^2$, and trying to see how the distance remains unchanged for an arbitrary time $t$. Any idea on how one might proceed?