In Michael Dummett's book "Elements of Intuitionism", the product of real numbers is defined as follow:

$x\cdot y= \{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$, where $\langle r_n\rangle ,\langle s_n\rangle$ are Cauchy sequences of rational numbers, and $\langle r_n\rangle \cdot \langle s_n\rangle=\langle r_n\cdot s_n\rangle$.

This definition is valid iff we can prove intuitionistically $\{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$ is indeed a real number, i.e. $\{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle s_n\rangle\in y \}$ is closed under "equivalent" (we say that $\langle r_n\rangle$ is equivalent to $\langle s_n\rangle$ if for any natural number $k$, we can find a natural number $n$ such that $|r_m-s_m|<2^{-k} $ for all $m>n$ ). This is to say, we must prove the following proposition intuitionistically:

Let $\langle r_n\rangle , \langle s_n\rangle , \langle t_n\rangle $ be Cauchy sequences of rational numbers, and $\langle t_n\rangle $ is equivalent to $\langle r_n\rangle \cdot \langle s_n\rangle$. Then we can construct two Cauchy sequences $\langle r_n'\rangle , \langle s_n'\rangle $ of rational numbers such that

(1) $\langle r_n'\rangle$ is equivalent to $\langle r_n\rangle$;

(2) $\langle s_n'\rangle$ is equivalent to $\langle s_n\rangle$;

(3) $\langle t_n\rangle =\langle r_n'\rangle \cdot \langle s_n'\rangle$.

But Michael Dummett doesn't justify his definition, and I find it's very difficult to prove the above proposition intuitionistically. Could you help me?

reallyneeded to ensure the function is well-defined is that $\langle r_n\cdot s_n\rangle$ is equivalent to $\langle r'_n\cdot s'_n\rangle$ whenever $\langle r_n\rangle$ is equivalent to $\langle r'_n\rangle$ and $\langle s_n\rangle$ is equivalent to $\langle s'_n\rangle$, but this should be straightforward to prove. – Emil Jeřábek Dec 3 '12 at 15:40