A finite endpoint of a maximal unit-speed geodesic produces a Cauchy curve

Fix $r\in I$. For every $t\in I$, the restriction of $\gamma$ between $r$ and $t$, affinely reparametrized to $[0,1]$, is a path from $\gamma (r)$ to $\gamma (t)$. Thus the image of $\gamma$ lies in the path component of $\gamma (r)$ and hence in the single connected component $C$; openness from [F1] makes every restricted segment a curve in the Riemannian manifold $C$.

If $s<t$ are in $I$, the unit-speed hypothesis and [F3] give $L_g(\gamma {\mathrm{\mid }}_{[s,t]})={\int }_s^{t}1du=t-s\mathrm{.}$ Applying [F2] in $C$ therefore yields $d_C(\gamma (s),\gamma (t))\le t-s=\mathrm{\mid }t-s\mathrm{\mid }\mathrm{.}$ The same inequality for $t<s$ follows by interchanging the two parameters, and equality of the parameters gives distance zero.

Let $\epsilon >0$ and put $T=\max \{r,b-\epsilon \mathrm{/}2\}$. Both entries of the maximum are less than $b$, so $T\in I$. If $T<s,t<b$, then $\mathrm{\mid }s-t\mathrm{\mid }<b-T\le \epsilon \mathrm{/}2<\epsilon$; step 2.1 gives $d_C(\gamma (s),\gamma (t))<\epsilon$. This is exactly the displayed Cauchy condition.

Maximality was not needed, so the special case for a maximal geodesic is immediate. If $a>-\mathrm{\infty }$, the curve $u\mapsto \gamma (-u)$ is again unit speed on $(-b,-a)$, and step 3.1 at its finite right endpoint $-a$ gives the stated left-endpoint version. The empty manifold admits no curve with nonempty domain; in dimension zero there is no unit-speed curve, while dimension one is covered unchanged. The assumptions $I\mathrm{\ne }\mathrm{\varnothing }$ and $b<\mathrm{\infty }$ exclude an empty source and an infinite endpoint; arbitrarily small positive $\epsilon$ is handled explicitly. No choice principle is used: $r$ is one fixed witness from the given nonempty interval and $T$ is a formula.