Correctness of proof by induction for proving correctness of polynomial evaluation algorithm

This excercise is from The Algorithm Design Manual by Skiena:

My solution is this:

We will attempt a proof by induction.

1. First, prove that the algorithm is correct for $n = 1$ :

$n = 1$ means that $p$ will be set to $a_1$. Then, the for loop will execute once with $i = 0$, setting $p$ to $a_1x + a_0$ and returning that value, which is correct for any $x$.

2. Now let's assume that the algorithm returns the correct value for $n=k$. This means that when $n=k$, the function will return $a_kx^k+a_{k-1}x^{k-1}+...+a_1x+a_0$. This is done in the function by setting the first $p$ to $a_k$ and then iterating over the for loop from k-1 to 0.

3. Now to prove that if $n=k$ yields a correct answer, so does $n=k+1$:

Let's follow the code execution for $n=k+1$. In the first row, $p$ is set to $a_{k+1}$. Then, in the first execution of the for loop, we have $i=k$ and we set $p$ to $a_{k+1}x+a_k$. After that, we have from k-1 to 0 iterations left, which is the total amount of iterations for $n=k$. $n=k$ gave us $a_kx^k+a_{k-1}x^{k-1}+...+a_1x+a_0$ with the first $p$ set to $a_k$ and from k-1 to 0 iterations. Now we have the same thing, but the first $p$ is set to $a_{k+1}x+a_k$. We can therefore substitute this into the function result for $n=k$: $(a_{k+1}x+a_k)x^k+a_{k-1}x^{k-1}+...+a_1x+a_0=a_{k+1}x^{k+1}+a_kx^k+...+a_1x+a_0$, which is the correct result. We have thus proven, by induction, that the algorithm is correct for any $n\geq1$.

Is this correct? I'm particularly unsure about the substitution of $a_{k+1}x+a_k$ into the function result for $n=k$, is this substitution correct?