Convergence of the rescaled power iterates

The declaration states a convergence claim about iterating a self-adjoint linear operator, phrased as follows. Fix a scalar field $\mathbb{k}$ that is either $\mathbb{R}$ or $\mathbb{C}$ (an instance of the RCLike class), and a finite-dimensional inner product space $E$ over $\mathbb{k}$; let $T:E\to E$ be a linear map that is self-adjoint (symmetric) with respect to the inner product. Let $n\in\mathbb{N}$ be given together with a hypothesis identifying it with $\dim_{\mathbb{k}}E$. Since $T$ is self-adjoint on this finite-dimensional space, it comes with an associated list of $n$ real eigenvalues $\lambda_0,\dots,\lambda_{n-1}$ (indexed by $j$ ranging over $\{0,\dots,n-1\}$) and an associated orthonormal basis $e_0,\dots,e_{n-1}$ of $E$ with $Te_j=\lambda_j e_j$ for each $j$; these are fixed data determined by $T$ and by the chosen identification of $\dim_{\mathbb k}E$ with $n$, not further hypotheses. An arbitrary vector $x_0\in E$ is fixed, and so is a distinguished index $i_0\in\{0,\dots,n-1\}$ — note that supplying such an index forces $n\ge 1$. Three hypotheses are imposed: (a) for every index $j\ne i_0$ in $\{0,\dots,n-1\}$, $|\lambda_j|<|\lambda_{i_0}|$, i.e. the eigenvalue at index $i_0$ strictly exceeds in absolute value every other eigenvalue on the list (so no other index attains the same absolute value, and this condition is vacuously true when $n=1$, since then there is no $j\ne i_0$); (b) $\lambda_{i_0}\ne 0$, stated as its own hypothesis even though, whenever $n\ge2$, it already follows from (a); and (c), writing $x_0=\sum_{j=0}^{n-1}c_j e_j$ for the unique coordinates $c_j\in\mathbb{k}$ of $x_0$ with respect to the basis $(e_j)$, that $c_{i_0}\ne0$. Given all of this, the conclusion asserts that the sequence of vectors $\big(\lambda_{i_0}^{k}\big)^{-1}\cdot\big(T^{k}x_0\big)\in E$, indexed by $k\in\mathbb{N}$ and tending toward $k\to\infty$ (with respect to the atTop filter on $\mathbb{N}$ and the norm-induced topology on $E$), converges to the fixed vector $c_{i_0}\cdot e_{i_0}$; here $T^kx_0$ means $T$ applied $k$ times to $x_0$, $\lambda_{i_0}^k$ is regarded as an element of $\mathbb{k}$ via the canonical real-to-$\mathbb{k}$ cast, its inverse is the field inverse in $\mathbb{k}$ (which, because $\lambda_{i_0}\ne0$ and hence $\lambda_{i_0}^k\ne0$ for every $k$, is always the genuine multiplicative inverse and never invokes the field's convention $0^{-1}=0$), and both "$\cdot$" symbols denote scalar multiplication of a vector of $E$ by a scalar in $\mathbb{k}$. As given, this theorem's proof term is sorry, so no proof of this claim is supplied in the code shown.