Spectral decomposition of power iterates

This declaration states, for a scalar field $\mathbb{k}$ that is either the real or complex numbers, a finite-dimensional inner-product space $E$ over $\mathbb{k}$, a natural number $n$ equal to the dimension of $E$, and a linear operator $T:E\to E$ that is self-adjoint (i.e. $\langle Tx,y\rangle=\langle x,Ty\rangle$ for all $x,y\in E$) — all of these being fixed background data (implicit types/instances plus the explicit hypothesis that $T$ is self-adjoint and the explicit hypothesis that $\dim E=n$) — that there is an associated orthonormal basis $e_0,\dots,e_{n-1}$ of $E$ consisting of eigenvectors of $T$, with corresponding real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ satisfying $Te_i=\lambda_i e_i$ for each index $i$ (with $\lambda_i$ understood as embedded into $\mathbb{k}$ where needed), and that for every vector $x_0\in E$ and every natural number $k$ (so $k$ ranges over $0,1,2,\dots$, with no positivity assumption), writing $x_0=\sum_i c_i e_i$ for the unique coordinates $c_i\in\mathbb{k}$ of $x_0$ in this basis, the $k$-fold self-composition of $T$ applied to $x_0$ equals $\sum_i (c_i\lambda_i^{k})\,e_i$, i.e. $T^k x_0=\sum_{i} c_i\lambda_i^{k}\,e_i$. Both $x_0$ and $k$ are universally quantified, so the claim covers the degenerate case $k=0$, where $T^0$ is the identity map and the asserted equation reduces (since $\lambda_i^0=1$) to the tautological basis expansion $x_0=\sum_i c_i e_i$; it also covers $\lambda_i=0$ for some or all $i$, in which case those terms vanish for $k\ge 1$; and it covers $n=0$, where $E$ is the trivial space, $x_0$ is forced to be $0$, and both sides of the equation are the empty sum, $0$. The statement itself asserts nothing about the eigenvalues being sorted, distinct, or nonzero, nor about $x_0$ or $T$ being nonzero. Finally, the proof of this theorem is literally the placeholder sorry, meaning no actual proof has been supplied — the equality is asserted in the code but not established by it.