Let $X$ be an $n$-dimensional differentiable manifold ($n\ge1$). A Riemannian metric in $X$ is a family $\{g_p\,|\,p\in X\}$, where for all $p\in X$:
$g_p:T_pX\times T_pX\to\mathbb{R}$ is an inner product for all $p\in X$,
and for every differentiable chart $(U,h,V)$ for $X$ at $p$ with coordinates $(x_1,\ldots,x_n)$ in $V$, the map $g_{ij}:U\to\mathbb{R}, g_{ij}(p)=\left(\frac{\partial}{\partial x_i}(p),\frac{\partial}{\partial x_i}(p)\right)$ is differentiable for each $i,j\in\{1,\ldots,n\}$ (here $\left\{\frac{\partial}{\partial x_i}(p)\,1\le i\le n\right\}$ is a basis for $T_pX$).
A differentiable map $\gamma:[a,b]\to X$ is said to be differentiable curve if there exists some $\epsilon_\gamma>0$ and a differentiable curve $\tilde\gamma:(a-\epsilon_\gamma,b+\epsilon_\gamma)\to X$ such that $\tilde\gamma|_{[a,b]}=\gamma$.
I showed that a differentiable curve $\gamma$ defined on a closed interval defines a geometric tangent vector $[\gamma](t)\in T_pX$ for all $t\in[a,b]$; for $t\in(a,b)$ this is nearly trivial, and for $t\in\{a,b\}$ I used the differentiable extension and the fact that the left and right limits coincide, to show that the value of the derivative of the constructed curve is determined by $\gamma$, i.e. \begin{align} [\gamma](t)=\begin{cases} [\mu_t^\epsilon],\quad\text{if }t\in(a,b), \\ [\tilde\mu_t^\epsilon],\quad\text{if }t\in\{a,b\}, \end{cases} \end{align} where $\epsilon\in(0,\epsilon_\gamma)$, $\mu_t^\epsilon=\gamma\circ\iota_t^\epsilon\circ T_t^\epsilon$, and $\tilde\mu_t^\epsilon=\tilde\gamma\circ\iota_t^\epsilon\circ T^\epsilon_t$; here $T_t^\epsilon:(-\epsilon,\epsilon)\to(t-\epsilon,t+\epsilon)$ is the translation and $\iota_t^\epsilon:(t-\epsilon,t+\epsilon)\to(a-\epsilon_\gamma,b+\epsilon_\gamma)$ is the inclusion.
I now have to show that the length \begin{align} L(\gamma)=\int_a^b\sqrt{g_{\gamma(t)}([\gamma](t),[\gamma](t)}\,\mathrm{d}t \end{align} satisfies the property $L(\gamma)=L(\gamma\circ f)$, where $f:[c,d]\to[a,b]$ is some diffeomorphism. Of course this comes down to the substitution rule for integrals, as the derivative of $f$ comes out of the square root. For $t'\in(c,d)$ you can also write down this down explicitly, since, letting $[\alpha_{t'}^\epsilon]$ be the geometric tangent vector defined by $\gamma\circ f$, we have for any chart $(U,h,v)$ at $h(\gamma(f(t'))$ (by the chain rule) \begin{align} \frac{\mathrm{d}}{\mathrm{d}t}(h\circ\alpha_t^\epsilon)(0)&=\lim_{k\to0}\frac{(h\circ\gamma\circ f)(t'+k)-(h\circ\gamma\circ f)(t')}{k} \\ &=\frac{\mathrm{d}}{\mathrm{d}t}(h\circ\gamma\circ f)(t') \\ &=\frac{\mathrm{d}}{\mathrm{d}t}(h\circ\gamma)(f(t'))\cdot Df(t'). \end{align} Now $Df(t')>0$ or $Df(t')<0$ for all $t'\in(c,d)$, so this comes out nicely out of the square root. For $t'\in\{c,d\}$ though, I'm somewhat puzzled. You use the differentiable extension $\hat{\gamma}$ of $\gamma\circ f$ to define $\alpha_{t'}^\epsilon$, and the value of derivative at zero of $h\circ\alpha_{t'}^\epsilon$ is (by the right and left limit coinciding argument) determined by $\gamma\circ f$, but here we cannot write down $Df(t')$ as before, since it is only the right (or left) limit!
Now my first thought was: Ah, I know measure theory, and those boundary points constitute a set of measure zero, so that doesn't count anyway. However even if this thought can be formalized, I would like to know if there is a formal way out of this that sticks to just using the chain rule and the things given/already done. Any help/thoughts are appreciated.