Sufficiently short geodesic segments are uniquely minimizing

By [F4], the component $C_p$ is open, connected, and itself a boundaryless Riemannian manifold; all competitors from $p$ to a point of $U$ remain in $C_p$. The local exponential map and curve lengths agree with those for the restricted metric, so [F2] is applicable there and the distance in the Statement is well-defined. By [F1], $\gamma (t)={\exp }_p(tv)$ on $[0,1]$. Since $\mathrm{\mid }tv\mathrm{\mid }\le \mathrm{\mid }v\mathrm{\mid }<\rho$, its image lies in $U$. The radial calculation in [F2] gives $L_g(\gamma )=\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$, and the componentwise local distance formula gives $d_g(p,\gamma (1))=\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$, so $\gamma$ attains the infimum over all piecewise $C^1$ competitors and hence over the piecewise smooth ones.

Let $c$ be a piecewise smooth curve in $M$ with the same endpoints and $L_g(c)=\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$. Its connected image lies in $C_p$ by [F4]. If its image left $U$, the strict clause of [F2] applied on $C_p$ would give $L_g(c)>\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$, a contradiction. Hence $c$ lies in $U$, and the equality characterization in [F2] says that, for $v\mathrm{\ne }0$, it is exactly a continuous piecewise smooth nondecreasing radial reparametrization from radius $0$ to radius $\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$ in the direction $v\mathrm{/}\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$. Conversely, every such reparametrization has length $\mathrm{\mid }v{\mathrm{\mid }}_{g_p}$ by [F2]. For $v=0$, [F2] says equality occurs exactly for the constant curve. This proves both uniqueness directions.

For the consequence, fix $p$, with no connectedness assumption on $M$. By [F3], choose the one supplied normal source $D\subseteq T_{p}M$ and instantiate one basis of the finite-dimensional tangent space; Gram--Schmidt gives an orthonormal basis. The coordinate image of $D$ is open about $0$, so it contains $B_{{\rho }_p}(0)$ for some witness ${\rho }_p>0$. Thus $B_{{\rho }_p}(0_p)\subseteq D$, and restriction makes ${\exp }_p:B_{{\rho }_p}(0_p)\to W_p:={\exp }_p(B_{{\rho }_p}(0_p))$ a diffeomorphism onto an open neighbourhood of $p$. By [F4], $W_p\subseteq C_p$ and all competitor curves from $p$ stay in $C_p$; hence steps 1.1--2.1 apply to every $\mathrm{\mid }v{\mathrm{\mid }}_{g_p}<{\rho }_p$ with distance understood on $C_p$.

Empty $M$ has no point $p$. In dimension zero, $T_{p}M=\{0_p\}$ and only the constant case occurs; choose any ${\rho }_p>0$ since the tangent ball and its image are singletons. In dimension one the two possible radial directions are distinguished by $v$. On a disconnected $M$, the connected component $C_p$ is canonical, open, and contains every competitor curve from $p$, so neither the distance notation nor the global uniqueness claim compares points in different components. The strict inequality $\mathrm{\mid }v\mathrm{\mid }<\rho$ excludes the sphere endpoint and ensures every $tv$, including $t=0,1$, stays in the source ball. The zero vector, constant curve, and possible pauses in a nonzero monotone reparametrization were treated in step 2.1. Both equality directions were proved there. Assumption [A1] is inherited through [F1]--[F3]; [F4] and choosing finitely at one fixed point add no choice principle.