The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse

The integrand $h$ of [L1] is continuous on $I$; for each $s\in I$ choose reals $\alpha <\beta$ with $[\alpha ,\beta ]\subseteq I$, $s\in [\alpha ,\beta ]$ and $s_0\in [\alpha ,\beta ]$, where $s$ is an endpoint of $[\alpha ,\beta ]$ only when it is an endpoint of $I$; then for $t\in [\alpha ,\beta ]$ oriented additivity [L6] gives $\tau (t)=c^{-1}{\int }_{s_0}^t\sqrt{g_x}=c^{-1}(F(t)-F(s_0))$ with $F(t):={\int }_{\alpha }^t\sqrt{g_x}$.

By the first fundamental theorem [L3], $F$ is differentiable on $[\alpha ,\beta ]$ with $F^{\mathrm{\prime }}=\sqrt{g_x}$ (one-sided at the endpoints), so $\tau$ is differentiable at $s$ with ${\tau }^{\mathrm{\prime }}(s)=c^{-1}\sqrt{g_x(s)}=c^{-1}\sqrt{-\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))}$; since $s\in I$ was arbitrary this holds at every point of $I$ with the one-sided reading at endpoints of $I$, and ${\tau }^{\mathrm{\prime }}$ is continuous on $I$ by [L4].

For every $s\in I$ the tangent $x^{\mathrm{\prime }}(s)$ is future timelike, so $\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))<0$ by [L5] and ${\tau }^{\mathrm{\prime }}(s)=c^{-1}\sqrt{-\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))}>0$.

For $a<b$ in $I$, oriented additivity [L6] gives $\tau (b)-\tau (a)=c^{-1}{\int }_a^b\sqrt{g_x}={\int }_a^b{\tau }^{\mathrm{\prime }}$ (using step 2.1 for the integrand); this is $\ge 0$ by monotonicity [L7]. If it were $0$, the continuous nonnegative function ${\tau }^{\mathrm{\prime }}$ would vanish identically on $[a,b]$ by [L8], contradicting its strict positivity on $[a,b]$ from step 3.1; hence $\tau (b)>\tau (a)$, so $\tau$ is strictly increasing and injective.

The image $J=\tau [I]$ is order-convex by [L9] applied to the continuous $\tau$, and it has at least two elements because $I$ is nondegenerate and $\tau$ is injective by step 4.1; hence $\tau :I\to J$ is a bijection.

The inverse $\rho :J\to I$ is strictly increasing and continuous on $J$ by the continuous-inverse theorem [L10], applied to the continuous injective $\tau$ on the order-convex set $I$.

For $b=\tau (s)\in J$ one has ${\tau }^{\mathrm{\prime }}(s)>0$ by step 3.1, so clause 1 of the inverse-derivative theorem [L11] gives that $\rho$ is differentiable at $b$ with ${\rho }^{\mathrm{\prime }}(b)=1\mathrm{/}{\tau }^{\mathrm{\prime }}(s)=c\mathrm{/}\sqrt{-\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))}>0$.

The function ${\rho }^{\mathrm{\prime }}$ equals $1\mathrm{/}({\tau }^{\mathrm{\prime }}\circ \rho )$ on $J$: for $b\in J$, ${\rho }^{\mathrm{\prime }}(b)=1\mathrm{/}{\tau }^{\mathrm{\prime }}(\rho (b))$ by step 7.1. The composite ${\tau }^{\mathrm{\prime }}\circ \rho$ is continuous on $J$ (composition of the continuous maps $\rho$ and ${\tau }^{\mathrm{\prime }}$ of steps 6.1 and 2.1) and strictly positive there, so its reciprocal is continuous by the quotient clause of the algebra of continuous functions; hence $\rho$ is continuously differentiable ($C^1$) on $J$.

Fix an inertial frame with chart $x_A$ and coordinate path $y=x_A\circ x$, and write $E$ for the linear frame isomorphism. For each $j$ the composite $y^j\circ \rho$ is differentiable on $J$ with derivative $(y^{j^{\mathrm{\prime }}}\circ \rho ){\rho }^{\mathrm{\prime }}$ by the chain rule [L12] (with the one-sided reading at endpoints), and this derivative is continuous as a product of the continuous functions $y^{j^{\mathrm{\prime }}}\circ \rho$ and ${\rho }^{\mathrm{\prime }}$ of steps 6.1 and 8.1; by the componentwise characterisation [L12], $y\circ \rho$ is therefore $C^1$ with $(y\circ \rho {)}^{\mathrm{\prime }}=(y^{\mathrm{\prime }}\circ \rho ){\rho }^{\mathrm{\prime }}$.

If $o$ is the frame origin, then $x\circ \rho =o+E(y\circ \rho )$; its displacement difference quotients are $E$ applied to those of $y\circ \rho$. By linearity and the chart derivative identification, step 9.1 and [L15] give $(x\circ \rho {)}^{\mathrm{\prime }}={\rho }^{\mathrm{\prime }}\cdot (x^{\mathrm{\prime }}\circ \rho )$; at $b=\tau (s)$ this reads $(x\circ \rho {)}^{\mathrm{\prime }}(\tau (s))={\rho }^{\mathrm{\prime }}(\tau (s))x^{\mathrm{\prime }}(s)=x^{\mathrm{\prime }}(s)\mathrm{/}{\tau }^{\mathrm{\prime }}(s)=c{x}^{\mathrm{\prime }}(s)\mathrm{/}\sqrt{-\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))}$ by step 7.1.

At each $b=\tau (s)\in J$, bilinearity [L15] and step 3.1 give $\eta ((x\circ \rho {)}^{\mathrm{\prime }}(b),(x\circ \rho {)}^{\mathrm{\prime }}(b))={\rho }^{\mathrm{\prime }}(b{)}^2\eta (x^{\mathrm{\prime }}(s),x^{\mathrm{\prime }}(s))<0$, so the tangent is timelike; and it is the positive multiple ${\rho }^{\mathrm{\prime }}(b)\cdot x^{\mathrm{\prime }}(s)$ of the future timelike vector $x^{\mathrm{\prime }}(s)$, with ${\rho }^{\mathrm{\prime }}(b)>0$, so by the coordinate description of the future cone [L5] it is future timelike. Hence $y=x\circ \rho$ is a $C^1$ future timelike worldline.

Let ${\tau }_y$ be the proper-time function of $y$ with base point $\tau (s_0)$ (defined by [L1] since $J$ is order-convex and $y$ is a $C^1$ future timelike worldline by step 11.1). Applying step 2.1 to $y$ gives ${\tau }_y^{\mathrm{\prime }}(b)=c^{-1}\sqrt{-\eta (y^{\mathrm{\prime }}(b),y^{\mathrm{\prime }}(b))}$ for $b\in J$, and by steps 7.1, 10.1 and [L15] this equals $c^{-1}{\rho }^{\mathrm{\prime }}(b)\sqrt{-\eta (x^{\mathrm{\prime }}(\rho (b)),x^{\mathrm{\prime }}(\rho (b)))}={\rho }^{\mathrm{\prime }}(b){\tau }^{\mathrm{\prime }}(\rho (b))=1$. Hence the function $\sigma (b):={\tau }_y(b)-b$ is continuous on $J$ and differentiable at every interior point with ${\sigma }^{\mathrm{\prime }}=0$ by the algebra of derivatives [L13], so $\sigma$ is constant by [L14]; therefore ${\tau }_y(b)-{\tau }_y(b_0)=b-b_0$ for all $b,b_0\in J$: the reparametrized worldline is parametrized by its own proper time up to the additive constant $\tau (s_0)$.

Every step uses one-dimensional or finite-dimensional calculus and fixed objects of the given worldline: the only "selections" are of the compact interval $[\alpha ,\beta ]$ around each point, made explicitly from the data, and no choice principle is used.