 Independence of finite presentation from finite generators

Suppose $G=⟨Y\mid R(Y)⟩$ is a finite group presentation, and $X$ is any finite generating set. Write $y_j=u_j(X)$ and $x_i=v_i(Y)$. A finite presentation on $X$ is obtained using the relators $R(u(X))$ and $x_i=v_i(u(X))$. The substitutions in both directions give inverse homomorphisms, proving that finite presentability does not depend on the finite generators chosen.

// Target: geometry-and-topology.bigb