[proofplan] Existence is proved by Gram--Schmidt orthogonalisation applied to the monomial basis $\{1, x, x^2, \dots\}$: at each stage, subtract projections onto the previously constructed orthogonal polynomials, producing a monic polynomial of degree $n$ orthogonal to all lower-degree polynomials. Uniqueness follows from positive definiteness: if two monic orthogonal polynomials of the same degree existed, their difference would have lower degree, be orthogonal to itself, and hence vanish. The basis property follows from linear independence of polynomials of distinct degrees. [/proofplan] [step:Construct $p_n$ by Gram--Schmidt orthogonalisation] Set $p_0(x) = 1$. For $n \ge 1$, define \begin{align*} p_n(x) &= x^n - \sum_{k=0}^{n-1} \frac{\langle x^n, p_k \rangle}{\langle p_k, p_k \rangle}\,p_k(x). \end{align*} Each $p_k$ with $k < n$ has $\langle p_k, p_k \rangle > 0$ by positive definiteness (since $p_k \neq 0$), so the formula is well-defined. By construction $p_n$ is monic of degree $n$, and for $0 \le j \le n-1$: \begin{align*} \langle p_n, p_j \rangle &= \langle x^n, p_j \rangle - \sum_{k=0}^{n-1} \frac{\langle x^n, p_k \rangle}{\langle p_k, p_k \rangle}\,\langle p_k, p_j \rangle = \langle x^n, p_j \rangle - \frac{\langle x^n, p_j \rangle}{\langle p_j, p_j \rangle}\,\langle p_j, p_j \rangle = 0, \end{align*} using the inductive hypothesis that $\langle p_k, p_j \rangle = 0$ for $k \neq j$ with $k, j < n$. [/step] [step:Prove uniqueness via positive definiteness] Suppose $q_n$ is another monic polynomial of degree $n$ orthogonal to $P_{n-1}[x]$. Then $p_n - q_n$ has degree $\le n-1$ (the leading terms cancel) and satisfies $\langle p_n - q_n, r \rangle = \langle p_n, r \rangle - \langle q_n, r \rangle = 0$ for all $r \in P_{n-1}[x]$. Taking $r = p_n - q_n$ gives $\langle p_n - q_n, p_n - q_n \rangle = 0$, so $p_n - q_n = 0$ by positive definiteness. [/step] [step:Verify the basis property from linear independence of distinct degrees] The set $\{p_0, \dots, p_n\}$ consists of $n+1$ polynomials of distinct degrees $0, 1, \dots, n$ in $P_n[x]$, which has dimension $n+1$. Since polynomials of distinct degrees are linearly independent (the leading terms cannot cancel in a nontrivial linear combination), $\{p_0, \dots, p_n\}$ is a basis for $P_n[x]$. [/step]