[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\}$.
[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]
[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]
