1: \begin{proof}

2: 

3: To show `$\ge$' we need to exhibit $r$ algebraically independent elements of $\RR[{\bf x}]^{G'}$. Letting $f_1,\ldots,f_{\tilde r}$ be a transcendence basis for $\RR[{\bf \tilde x}]^{\tilde G}$, it suffices to take

4: $$I \defeq \{f_i({\bf x}^{(k)})\}_{1 \le i \le \tilde r, 1 \le k \le K} \cup \{z_1,\ldots,z_{K-1}\}.$$

5: 

6: % rigorous proof that these are alg indep? (disjoint sets of variables)

7: % just think about Jacobian -- block diagonal

8: 

9: To show `$\le$' we first recall that we can obtain a spanning set for the subspace $\RR[{\bf x}]^{G'}_d$ by applying the Reynolds operator $\mathcal{R}$ (for $G'$) to each degree-$d$ monomial (in the variables ${\bf x}$). Such a monomial takes the form

10: $$m({\bf x}) = M({\bf z}) \prod_{k=1}^K m_k({\bf x}^{(k)})$$

11: where $M, m_k$ are monomials. Applying the Reynolds operator yields

12: $$\mathcal{R}(m({\bf x})) = \Ex_{g_1,\ldots,g_k \sim \tilde G} M({\bf z}) \prod_{k=1}^K m_k(g_k \cdot {\bf x}^{(k)}) = M({\bf z}) \prod_{k=1}^K \Ex_{g_k \sim \tilde G} m_k(g_k \cdot {\bf x}^{(k)}).$$

13: Note that $\mathcal{R}(m({\bf x}))$ is the product of \emph{pure} invariants, i.e.\ invariants that only involve variables from a single one of the blocks ${\bf x}^{(1)}, \ldots, {\bf x}^{(K)}, {\bf z}$. It is clear that $I$ (from above) is a maximal set of algebraically independent pure invariants. It is now easy to show using the Jacobian criterion (Proposition~\ref{prop:jac}) that if any $\mathcal{R}(m({\bf x}))$ is added to $I$, it will no longer be algebraically independent. The result now follows using basic properties of algebraic independence (Proposition~\ref{prop:exchange} and Lemma~\ref{lem:basis}).

14: \end{proof}

15: