[proofplan]
The proof is the standard shifted-trajectory argument. Starting from a feasible horizon-$N$ plan at $x$, exactness of the model identifies the actual successor $x^+$ with the first predicted successor $x_1^*$. We then form a new horizon-$N$ candidate at $x^+$ by dropping the already-applied input, shifting the remaining planned inputs forward, and appending the terminal feedback input $\kappa_f(x_N^*)$. Terminal invariance of $X_f$ under $\kappa_f$ supplies the new terminal constraint, while all intermediate constraints follow from the old feasible trajectory.
[/proofplan]
[step:Identify the exact closed-loop successor with the first predicted state]
Because $(u_0^*,\dots,u_{N-1}^*)$ and $(x_0^*,\dots,x_N^*)$ are feasible at $x$, we have $x_0^*=x$ and
\begin{align*}
x_1^* = F(x_0^*,u_0^*).
\end{align*}
Using $x_0^*=x$, the definition of the exact closed-loop successor gives
\begin{align*}
x^+ = F(x,u_0^*) = F(x_0^*,u_0^*) = x_1^*.
\end{align*}
Thus the state from which the next feasibility problem starts is exactly the first predicted successor from the old feasible plan.
[/step]
[step:Construct the shifted input and state candidates at $x^+$]
Define an input tuple $(v_0,\dots,v_{N-1}) \in U^N$ as follows: for each index $j \in \{0,\dots,N-2\}$, when this index set is nonempty, set $v_j := u_{j+1}^*$, and set
\begin{align*}
v_{N-1} := \kappa_f(x_N^*).
\end{align*}
The definition is meaningful also when $N=1$, because then the first index range is empty and the tuple consists only of $v_0=\kappa_f(x_1^*)$.
Define a state tuple $(y_0,\dots,y_N) \in X^{N+1}$ by setting $y_j := x_{j+1}^*$ for each $j \in \{0,\dots,N-1\}$ and
\begin{align*}
y_N := F(x_N^*,\kappa_f(x_N^*)).
\end{align*}
The tuple $(v_0,\dots,v_{N-1})$ lies in $U^N$: the entries $v_j=u_{j+1}^*$ lie in $U$ for $j \leq N-2$ because the old input tuple lies in $U^N$, and $v_{N-1}\in U$ because $\kappa_f:X_f\to U$ and $x_N^*\in X_f$. The tuple $(y_0,\dots,y_N)$ lies in $X^{N+1}$: the entries $y_j=x_{j+1}^*$ lie in $X$ for $j \leq N-1$ because the old state tuple lies in $X^{N+1}$, and $y_N\in X$ because $F:X\times U\to X$, $x_N^*\in X_f\subset X$, and $\kappa_f(x_N^*)\in U$.
[guided]
The new candidate should have length $N$, just like the old candidate, but it must begin at the new state $x^+$. The old first input $u_0^*$ has already been applied, so it cannot be reused as the first planned input for the next problem. The natural construction is therefore to shift the unused planned controls forward and append one terminal control at the end.
Define the new input tuple $(v_0,\dots,v_{N-1})$ by taking
$v_j := u_{j+1}^*$ for each $j \in \{0,\dots,N-2\}$, when this set is nonempty, and by setting
\begin{align*}
v_{N-1} := \kappa_f(x_N^*).
\end{align*}
This notation covers the edge case $N=1$: then there are no inherited controls $u_1^*,\dots,u_{N-1}^*$, and the new one-step input tuple is simply $(\kappa_f(x_1^*))$.
Now define the corresponding shifted state tuple $(y_0,\dots,y_N)$ by setting $y_j := x_{j+1}^*$ for each $j \in \{0,\dots,N-1\}$ and
\begin{align*}
y_N := F(x_N^*,\kappa_f(x_N^*)).
\end{align*}
We must check that these are admissible objects before checking the dynamics. For the inputs, if $j \leq N-2$, then $v_j=u_{j+1}^*\in U$ because the old input tuple belongs to $U^N$. The final input satisfies $v_{N-1}\in U$ because $x_N^*\in X_f$ and the terminal controller is a map $\kappa_f:X_f\to U$. Hence $(v_0,\dots,v_{N-1})\in U^N$.
For the states, if $j \leq N-1$, then $y_j=x_{j+1}^*\in X$ because the old state tuple belongs to $X^{N+1}$. The final state $y_N$ is also in $X$: indeed $x_N^*\in X_f\subset X$, $\kappa_f(x_N^*)\in U$, and the system map has codomain $X$, so
\begin{align*}
F(x_N^*,\kappa_f(x_N^*))\in X.
\end{align*}
Thus $(y_0,\dots,y_N)\in X^{N+1}$.
[/guided]
[/step]
[step:Verify the shifted trajectory satisfies the dynamics and terminal constraint]
First,
\begin{align*}
y_0 = x_1^* = x^+.
\end{align*}
For each $j \in \{0,\dots,N-2\}$, when this index set is nonempty, feasibility of the old trajectory gives
\begin{align*}
y_{j+1}=x_{j+2}^*=F(x_{j+1}^*,u_{j+1}^*)=F(y_j,v_j).
\end{align*}
For the last index $j=N-1$, the definition of $y_N$ and $v_{N-1}$ gives
\begin{align*}
y_N = F(x_N^*,\kappa_f(x_N^*)) = F(y_{N-1},v_{N-1}).
\end{align*}
Thus $y_{j+1}=F(y_j,v_j)$ for every $j \in \{0,\dots,N-1\}$.
Finally, since the old feasible trajectory satisfies $x_N^*\in X_f$ and the terminal invariance hypothesis gives $F(y,\kappa_f(y))\in X_f$ for every $y\in X_f$, applying it with $y=x_N^*$ yields
\begin{align*}
y_N=F(x_N^*,\kappa_f(x_N^*))\in X_f.
\end{align*}
[/step]
[step:Conclude horizon-$N$ feasibility at the successor]
The input tuple $(v_0,\dots,v_{N-1})\in U^N$ and the state tuple $(y_0,\dots,y_N)\in X^{N+1}$ satisfy $y_0=x^+$, the dynamics $y_{j+1}=F(y_j,v_j)$ for every $j\in\{0,\dots,N-1\}$, and the terminal constraint $y_N\in X_f$. Therefore the horizon-$N$ terminal-constrained feasibility problem at $x^+$ is feasible. By the definition of $\mathcal X_N$, this means
\begin{align*}
x^+ \in \mathcal X_N.
\end{align*}
[/step]
