Balls of a word metric are finite if and only if the generating set is finite

Given: The hypotheses of the Statement.

The word metric of $G$ with respect to $S$ is $d_S(g,h)=\mathrm{\mid }{g}^{-1}h{\mathrm{\mid }}_S$ (The word metric of a group with respect to a generating set).

The word length $\mathrm{\mid }g{\mathrm{\mid }}_S$ is the least $n$ such that $g$ is a product of $n$ elements of $S\cup S^{-1}$ (Word length of a group element with respect to a generating set).

The word metric is a left-invariant metric and coincides with the path metric of the Cayley graph (The word metric is a left-invariant metric and coincides with the path metric of the Cayley graph).

In a locally finite connected graph every ball of the path metric is finite (In a connected locally finite graph every ball of the path metric is finite).

Every vertex of a Cayley graph has the same degree, and the graph is locally finite exactly when the symmetrised generating set is finite (Cayley-graph neighbourhoods are equipotent, and local finiteness is equivalent to finiteness of the symmetrised subset).

$B(x,r)$ is the open ball, $\bar{B}(x,r)$ the closed ball and $S(x,r)$ the sphere of centre $x$ and radius $r$. The radius is always a strictly positive real; a ball of radius $0$ or of negative radius is never written in this library. (Open ball, closed ball and sphere in a metric space).

A set $A$ is finite when $A\approx n$ for some $n\in \mathbb{N}$. (The cardinality $\mid A\mid$ of a finite set).

A group is finitely generated when some finite subset generates it (Finitely generated groups).

Write ${\prod }_{i<m}{A}_i:=\{f:f\text{ is a function with domain }m\text{ and }f(i)\in A_i\text{ for every }i<m\}\mathrm{.}$ Then ${\prod }_{i<m}{A}_i$ is finite and $\mid {\prod }_{i<m}{A}_i\mid ={\prod }_{i<m}\mid A_i\mid$, the right-hand product being the $\mathbb{N}$-valued one of. (The product rule: $\mid A\times B\mid =\mid A\mid \mid B\mid$, and $\mid {\prod }_{i<m}{A}_i\mid ={\prod }_{i<m}\mid A_i\mid$).