@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$> .

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.