Every rapidly Cauchy sequence (\(d^\circ (u_k,u_{k+1}){\lt}2^{-k}\)) converges: this is Billingsley’s Theorem 12.2 via the \(\sigma _\infty \) infinite-composition argument, in which the composed time changes converge (geometric log-slope control) and the time-changed paths converge uniformly. Combined with separability — the countable dense family of step functions with rational cut points and rational values, produced from the partition lemma and a piecewise-linear time-change alignment — this makes \(D([0,1],\mathbb {R})\) a complete separable metric space, and the CompleteSpace, SecondCountableTopology and PolishSpace instances are installed.