In Michael Dummett's book "Elements of Intuitionism" , the product of real numbers are 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 all 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