[proofplan] The proof is the coordinate form of the standard reduction of an order-$m$ scalar equation to a first-order system. In the forward direction, the companion variables are defined as the successive derivatives of $y$, so differentiating the $i$th coordinate gives the next coordinate, and the last coordinate equation is exactly the original scalar equation. In the reverse direction, the equations $\dot x_i=x_{i+1}$ propagate by induction from $y=x_1$ to show $x_i=y^{(i-1)}$, and the final equation then gives the higher-order scalar equation. [/proofplan]

[step:Differentiate the companion coordinates to obtain the first-order system] Assume first that $y:J\to\mathbb{R}$ satisfies the hypotheses of the higher-order equation. Define the component functions \begin{align*} x_i:J\to\mathbb{R},\qquad x_i(t)=y^{(i-1)}(t) \end{align*} for each $i\in\{1,\ldots,m\}$. By the hypothesis \begin{align*} (y(t),\dot y(t),\ldots,y^{(m-1)}(t))\in V \end{align*} for every $t\in J$, the map $x:J\to V$ is well-defined. For $i\in\{1,\ldots,m-1\}$, the function $x_i=y^{(i-1)}$ is differentiable on $J$ because $y$ is $m$-times differentiable and $i\le m-1$. Its derivative is \begin{align*} \dot x_i(t)=\frac{d}{dt}y^{(i-1)}(t)=y^{(i)}(t)=x_{i+1}(t) \end{align*} for every $t\in J$. Similarly, $x_m=y^{(m-1)}$ is differentiable on $J$, and the assumed scalar equation gives \begin{align*} \dot x_m(t)=y^{(m)}(t)=G(t,y(t),\dot y(t),\ldots,y^{(m-1)}(t))=G(t,x_1(t),\ldots,x_m(t)) \end{align*} for every $t\in J$. Hence all coordinate functions of $x$ are differentiable and satisfy the displayed companion system, so $x:J\to V$ is a differentiable solution of the first-order system. [/step]

[step:Recover all companion coordinates from the first coordinate by induction]Assume conversely that $x:J\to V$ is differentiable and satisfies the companion system. Define \begin{align*} y:J\to\mathbb{R},\qquad y(t)=x_1(t). \end{align*} We prove by induction on $i\in\{1,\ldots,m\}$ that $y$ is $(i-1)$-times differentiable on $J$ and that \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} for every $t\in J$. For $i=1$, this is the definition of $y$, since $y^{(0)}=y=x_1$. Suppose now that $i\in\{1,\ldots,m-1\}$ and that \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} for every $t\in J$. The function $x_i:J\to\mathbb{R}$ is differentiable because $x:J\to V\subset\mathbb{R}^m$ is differentiable coordinatewise. The system equation gives \begin{align*} \frac{d}{dt}y^{(i-1)}(t)=\dot x_i(t)=x_{i+1}(t) \end{align*} for every $t\in J$. Thus $y^{(i-1)}$ is differentiable on $J$, so $y$ is $i$-times differentiable, and \begin{align*} y^{(i)}(t)=x_{i+1}(t) \end{align*} for every $t\in J$. This proves the induction step. Therefore \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} for every $t\in J$ and every $i\in\{1,\ldots,m\}$.[/step]

[guided]We start with the only scalar function that can possibly solve the higher-order equation, namely the first coordinate of the system. Define \begin{align*} y:J\to\mathbb{R},\qquad y(t)=x_1(t). \end{align*} The goal is to show that the remaining coordinates are not independent variables: the system forces $x_2$ to be $\dot y$, then $x_3$ to be $\ddot y$, and so on. We prove this precisely by induction on $i\in\{1,\ldots,m\}$. The induction statement is that $y$ is $(i-1)$-times differentiable and that \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} for every $t\in J$. When $i=1$, this is exactly the definition of $y$, because $y^{(0)}=y$ and $y=x_1$. Now assume the statement has been proved for some $i\in\{1,\ldots,m-1\}$. Thus \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} for every $t\in J$. Since $x:J\to V\subset\mathbb{R}^m$ is differentiable, each coordinate function $x_i:J\to\mathbb{R}$ is differentiable. Therefore the function $y^{(i-1)}$, which equals $x_i$, is differentiable. Using the $i$th equation of the first-order system, we obtain \begin{align*} \frac{d}{dt}y^{(i-1)}(t)=\dot x_i(t)=x_{i+1}(t) \end{align*} for every $t\in J$. This proves both parts needed for the next index: $y$ is $i$-times differentiable, and \begin{align*} y^{(i)}(t)=x_{i+1}(t) \end{align*} for every $t\in J$. By induction, the identity \begin{align*} x_i(t)=y^{(i-1)}(t) \end{align*} holds for every $t\in J$ and every $i\in\{1,\ldots,m\}$. This is the mechanism that converts the first-order companion system back into a single higher-order scalar equation.[/guided]

[step:Use the last coordinate equation to recover the scalar equation] From the previous step with $i=m$, we have \begin{align*} x_m(t)=y^{(m-1)}(t) \end{align*} for every $t\in J$. Since $x_m:J\to\mathbb{R}$ is differentiable, the function $y^{(m-1)}$ is differentiable, so $y$ is $m$-times differentiable on $J$. The last equation of the companion system gives \begin{align*} y^{(m)}(t)=\dot x_m(t)=G(t,x_1(t),\ldots,x_m(t)) \end{align*} for every $t\in J$. Substituting the identities $x_i(t)=y^{(i-1)}(t)$ for $i\in\{1,\ldots,m\}$ yields \begin{align*} y^{(m)}(t)=G(t,y(t),\dot y(t),\ldots,y^{(m-1)}(t)) \end{align*} for every $t\in J$. Also, since $x(t)\in V$ and $x(t)=(y(t),\dot y(t),\ldots,y^{(m-1)}(t))$, the required state constraint is satisfied. This proves the converse implication and completes the equivalence. [/step]