C² inverses and scalar return roots

Let $f$ be $C^2$ at $x_0$ with $Df(x_0)$ invertible; by [F1] there are open sets $V$ with $x_0\in V$ and $W$ with $f(x_0)\in W$ such that $f{\mathrm{\mid }}_V:V\to W$ is a bijection with $C^1$ inverse $g:W\to V$ satisfying $Dg(y)=Df(g(y){)}^{-1}$.

The matrix $Df$ is invertible throughout a neighbourhood of $g(W)$, and the entries of its inverse are quotients of polynomial functions of the entries of $Df$ by the determinant, hence are $C^1$ functions of the entries of $Df$; since $f$ is $C^2$ and $g$ is $C^1$, [F2] shows that $y\mapsto Dg(y)=Df(g(y){)}^{-1}$ is $C^1$, that is, $g$ is $C^2$.

Apply step 1.1 to the $C^2$ map $G(s,t):=(s,g(s,t))$ near $(s_0,t_0)$: its derivative $DG=\left(\begin{array}{cc}1& 0\\ g_s& g_t\end{array}\right)$ has determinant $g_t$, which is nonzero at $(s_0,t_0)$ by hypothesis, so $DG(s_0,t_0)$ is invertible and $G$ has a local $C^2$ inverse by step 2.1.

Write the second component of that local inverse as $t=T(s)$ with $T$ defined near $s_0$; then $G(s,T(s))=(s,0)$, that is $g(s,T(s))=0$, and the equality is unique among $t$ near $t_0$ because the local inverse of $G$ is a function.

Differentiating the identity $g(s,T(s))=0$ in $s$ with [F2] gives $g_s+g_t{T}^{\mathrm{\prime }}=0$ at $(s,T(s))$, hence $T^{\mathrm{\prime }}=-g_s\mathrm{/}{g}_t$ wherever $g_t\mathrm{\ne }0$, which holds near $s_0$.

Differentiating the same identity twice with [F2] gives $g_{ss}+g_{st}{T}^{\mathrm{\prime }}+g_t{T}^{\mathrm{\prime }\mathrm{\prime }}+(g_{ts}+g_{tt}{T}^{\mathrm{\prime }})T^{\mathrm{\prime }}=0$ at $(s,T(s))$; using $g_{st}=g_{ts}$ and solving for $T^{\mathrm{\prime }\mathrm{\prime }}$ because $g_t\mathrm{\ne }0$ yields $T^{\mathrm{\prime }\mathrm{\prime }}=-(g_{ss}+2g_{st}{T}^{\mathrm{\prime }}+g_{tt}(T^{\mathrm{\prime }}{)}^2)\mathrm{/}{g}_t$, and all steps used only the stated local inverse and chain rule, so no choice axiom is invoked.