[proofplan] We prove the estimate by induction on the positive integer $n$. The base case is exactly the contraction inequality applied to the pair $(x_0,x^*)$, using the fixed point identity $f(x^*)=x^*$. The induction step repeats the same contraction estimate at the points $f^n(x_0)$ and $x^*$, then inserts the inductive hypothesis to gain one additional factor of $c$. [/proofplan] [step:Verify the estimate for the first iterate] Fix $x_0 \in X$. Since $x^*$ is a fixed point of $f$, we have $f(x^*)=x^*$. Applying the contraction inequality to the points $x_0,x^* \in X$ gives \begin{align*} d(f(x_0),x^*) = d(f(x_0),f(x^*)) \le c\,d(x_0,x^*). \end{align*} Since $f^1=f$ and $c^1=c$, this is precisely the desired estimate for $n=1$. [guided] We start with the first iterate because Androma's convention is $\mathbb{N}=\{1,2,3,\dots\}$. The quantity we need to estimate when $n=1$ is $d(f^1(x_0),x^*)$, and by the definition of the first iterate this is $d(f(x_0),x^*)$. The fixed point hypothesis says exactly that $f(x^*)=x^*$. Therefore we may rewrite the second argument as an image under $f$: \begin{align*} d(f(x_0),x^*) = d(f(x_0),f(x^*)). \end{align*} Now the contraction hypothesis applies to the two points $x_0,x^* \in X$. It gives \begin{align*} d(f(x_0),f(x^*)) \le c\,d(x_0,x^*). \end{align*} Combining these equalities and inequalities, we obtain \begin{align*} d(f^1(x_0),x^*) \le c^1 d(x_0,x^*). \end{align*} This proves the base case. [/guided] [/step] [step:Propagate the estimate from one iterate to the next] Assume that, for some $n \in \mathbb{N}$, \begin{align*} d(f^n(x_0),x^*) \le c^n d(x_0,x^*). \end{align*} Using the identity $f^{n+1}(x_0)=f(f^n(x_0))$ and the fixed point identity $x^*=f(x^*)$, we have \begin{align*} d(f^{n+1}(x_0),x^*) = d(f(f^n(x_0)),f(x^*)). \end{align*} Applying the contraction inequality to the points $f^n(x_0),x^* \in X$ gives \begin{align*} d(f(f^n(x_0)),f(x^*)) \le c\,d(f^n(x_0),x^*). \end{align*} By the inductive hypothesis, \begin{align*} c\,d(f^n(x_0),x^*) \le c\,c^n d(x_0,x^*) = c^{n+1}d(x_0,x^*). \end{align*} Thus \begin{align*} d(f^{n+1}(x_0),x^*) \le c^{n+1}d(x_0,x^*). \end{align*} [/step] [step:Conclude the estimate for every positive iterate] The first step proves the assertion for $n=1$, and the second step proves that validity at an arbitrary $n \in \mathbb{N}$ implies validity at $n+1$. By induction on $\mathbb{N}$, for every $n \in \mathbb{N}$, \begin{align*} d(f^n(x_0),x^*) \le c^n d(x_0,x^*). \end{align*} Since $x_0 \in X$ was arbitrary, the estimate holds for every starting point $x_0 \in X$. This proves the theorem. [/step]