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?

-
The classical proof of the above proposition uses the fact " $\langle r_n\rangle$ is equivalent to 0 or not", but this fact isn't valid intuitionistically. –  Set Dec 3 '12 at 8:55
I don’t have Dummett’s book, but are you sure you are reading the definition correctly? Isn’t it simply defined as the equivalence class of $\langle r_n\cdot s_n\rangle$, which would make it closed under equivalence by definition? What is really needed 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
@Jeřábek Yes, I'm sure that it's defined as above in Dummett’s book (first edition in 1977). But I don't know whether he justify his definition in the second edition (in 2000) of the book. I'm also Surprised that he uses this definition. I consult other books about constructive analysis, such as Bishop's "Foundations of constructive analysis" and Troelstra's "Principles of Intuitionism" , the definition in these books are unlike the definition of Dummett’s, but it is the same as you say, defined as the equivalence class of <$r_n S_n$> . –  Set Dec 3 '12 at 17:02