Solution (source code)

= Solution

For $v\in T_pS$ sufficiently small, let $\gamma_v$ be the <geodesic> with $\gamma_v(0)=p$ and $\dot\gamma_v(0)=v$. Define $\exp_p(v)=\gamma_v(1)$. <Geodesic> uniqueness and rescaling give $\gamma_v(t)=\exp_p(tv)$, so
$$
d(\exp_p)_0(v)=\left.\frac{d}{dt}\exp_p(tv)\right|_{t=0}=v.
$$
Thus its derivative at zero is the identity, an isomorphism. Assuming the stated smoothness, the <inverse function theorem> proves \b[$\exp_p$ is a <diffeomorphism> between neighbourhoods of zero and $p$].