 Cauchy-sequence construction of a metric completion

For two Cauchy sequences, $|d(x_n,y_n)-d(x_m,y_m)|\le d(x_n,x_m)+d(y_n,y_m)$, so the displayed limit exists. It defines a pseudometric on the Cauchy sequences, and its metric quotient identifies sequences whose mutual distance tends to zero. Constant sequences embed the original metric space isometrically. Their image is dense, because the class of $(x_n)$ is approached by the constant classes of $x_n$. The quotient is complete: from a Cauchy sequence of its points select a subsequence whose successive distances are below $2^{-j}$ and choose original-space points within $2^{-j}$ of these subsequence points. Those original-space points form a Cauchy sequence and its class is the limit of the subsequence, hence of the whole sequence. The original embedding is onto exactly when the original space is complete.