[proofplan] We prove the contraction estimate directly from the definitions. For arbitrary points $x,y\in X$, first apply the contraction bound for $f$ to the two points $g(x)$ and $g(y)$, then apply the contraction bound for $g$ to the original pair $x,y$. Finally, we verify that the product $c_f c_g$ is still a number in $[0,1)$, so the product bound is a valid contraction constant for $f\circ g$. [/proofplan] [step:Apply the contraction estimate for $f$ after composing with $g$] Let $x,y\in X$ be arbitrary. Since $g:X\to X$, the points $g(x)$ and $g(y)$ belong to $X$. The contraction estimate for $f$ applied to the pair $g(x),g(y)\in X$ gives \begin{align*} d(f(g(x)),f(g(y))) \leq c_f d(g(x),g(y)). \end{align*} By the definition of composition, $(f\circ g)(x)=f(g(x))$ and $(f\circ g)(y)=f(g(y))$, so \begin{align*} d((f\circ g)(x),(f\circ g)(y)) \leq c_f d(g(x),g(y)). \end{align*} [guided] Fix arbitrary points $x,y\in X$. The goal is to estimate the distance between the two images of these points under the composite map $f\circ g:X\to X$. By definition of composition, \begin{align*} (f\circ g)(x)=f(g(x)) \end{align*} and \begin{align*} (f\circ g)(y)=f(g(y)). \end{align*} To use the contraction estimate for $f$, its two inputs must be points of $X$. This condition is satisfied because $g:X\to X$, hence $g(x)\in X$ and $g(y)\in X$. Applying the assumed contraction inequality for $f$ to the pair $g(x),g(y)$ yields \begin{align*} d(f(g(x)),f(g(y))) \leq c_f d(g(x),g(y)). \end{align*} Replacing $f(g(x))$ and $f(g(y))$ by the corresponding values of the composite map gives \begin{align*} d((f\circ g)(x),(f\circ g)(y)) \leq c_f d(g(x),g(y)). \end{align*} This reduces the desired estimate for $f\circ g$ to the known estimate for $g$. [/guided] [/step] [step:Apply the contraction estimate for $g$ and obtain the product bound] The contraction estimate for $g$ applied to the pair $x,y\in X$ gives \begin{align*} d(g(x),g(y)) \leq c_g d(x,y). \end{align*} Since $c_f\in[0,1)$, we have $c_f\geq 0$, so multiplying this inequality by $c_f$ preserves the inequality: \begin{align*} c_f d(g(x),g(y)) \leq c_f c_g d(x,y). \end{align*} Combining this with the estimate from the previous step gives \begin{align*} d((f\circ g)(x),(f\circ g)(y)) \leq c_f c_g d(x,y). \end{align*} [/step] [step:Verify that the product is a valid contraction constant] Because $c_f,c_g\in[0,1)$, we have $0\leq c_f<1$ and $0\leq c_g<1$. Therefore $0\leq c_f c_g$ and, since $c_f<1$ and $c_g<1$ with both factors non-negative, \begin{align*} c_f c_g < 1. \end{align*} Thus $c_f c_g\in[0,1)$. Since $x,y\in X$ were arbitrary, the estimate \begin{align*} d((f\circ g)(x),(f\circ g)(y)) \leq c_f c_g d(x,y) \end{align*} holds for all $x,y\in X$ with $c_f c_g\in[0,1)$. Hence $f\circ g:X\to X$ is a contraction with contraction constant $c_f c_g$. [/step]