[proofplan] We first prove the identity after restricting the $y$-variables to a finite set $y_1,\dots,y_r$. In that setting the Cauchy kernel factors as a product of the complete homogeneous generating series, so its expansion is indexed by exponent vectors in $\mathbb{N}^r$. Grouping exponent vectors by their decreasing rearrangement identifies the grouped monomials with the monomial symmetric functions and the coefficients with the products $h_\lambda$. Finally, the finite-variable identities are compatible under increasing $r$, so they determine the identity in the completed symmetric-function [tensor product](/page/Tensor%20Product). [/proofplan] [step:Restrict the Cauchy kernel to finitely many $y$-variables] Fix an integer $r \geq 1$. Let \begin{align*} \Omega_r(x;y_1,\dots,y_r) := \prod_{j=1}^{r}\prod_{i \geq 1}(1 - x_i y_j)^{-1} \end{align*} be the specialization of $\Omega(x,y)$ obtained by setting $y_j = 0$ for all $j > r$. For each indeterminate $t$, the defining generating series for the complete homogeneous symmetric functions is \begin{align*} \prod_{i \geq 1}(1 - x_i t)^{-1} = \sum_{a=0}^{\infty} h_a(x)t^a, \end{align*} with $h_0(x)=1$. Substituting $t = y_j$ for each $j \in \{1,\dots,r\}$ gives \begin{align*} \prod_{i \geq 1}(1 - x_i y_j)^{-1} = \sum_{a=0}^{\infty} h_a(x)y_j^a. \end{align*} Multiplying these $r$ identities in the formal [power series](/page/Power%20Series) ring with coefficients in $\widehat{\operatorname{Sym}}_x$, we obtain \begin{align*} \Omega_r(x;y_1,\dots,y_r) = \sum_{(a_1,\dots,a_r)\in \mathbb{N}^r} h_{a_1}(x)\cdots h_{a_r}(x) y_1^{a_1}\cdots y_r^{a_r}. \end{align*} [/step] [step:Group exponent vectors by their associated partition] For an exponent vector $a=(a_1,\dots,a_r)\in \mathbb{N}^r$, let $\lambda(a)$ denote the partition obtained by rearranging the nonzero entries of $a$ in weakly decreasing order. Conversely, for a partition $\lambda$, let $\lambda^{(r)}$ denote the length-$r$ vector obtained by appending zeros to $\lambda$ if $\ell(\lambda)\leq r$; if $\ell(\lambda)>r$, there is no exponent vector in $\mathbb{N}^r$ with associated partition $\lambda$. Since multiplication in $\operatorname{Sym}$ is commutative and $h_0(x)=1$, whenever $\lambda(a)=\lambda$ we have \begin{align*} h_{a_1}(x)\cdots h_{a_r}(x)=h_\lambda(x). \end{align*} Therefore the terms in the expansion of $\Omega_r$ with associated partition $\lambda$ contribute \begin{align*} h_\lambda(x) \sum_{\substack{a\in \mathbb{N}^r\\ \lambda(a)=\lambda}} y_1^{a_1}\cdots y_r^{a_r}. \end{align*} By definition, the finite-variable monomial symmetric function $m_\lambda(y_1,\dots,y_r)$ is exactly this sum when $\ell(\lambda)\leq r$, and it is $0$ when $\ell(\lambda)>r$. Hence \begin{align*} \Omega_r(x;y_1,\dots,y_r) = \sum_{\lambda} h_\lambda(x)m_\lambda(y_1,\dots,y_r), \end{align*} where the sum ranges over all partitions and only partitions of length at most $r$ contribute. [guided] The expansion from the previous step is indexed by ordered exponent vectors \begin{align*} a=(a_1,\dots,a_r)\in \mathbb{N}^r. \end{align*} The monomial symmetric basis, however, is indexed by partitions, not by ordered vectors. The bridge between these two index sets is sorting: define $\lambda(a)$ to be the partition obtained by deleting the zero entries of $a$ and arranging the remaining entries in weakly decreasing order. Now fix a partition $\lambda$. The exponent vectors $a\in \mathbb{N}^r$ satisfying $\lambda(a)=\lambda$ are precisely the distinct permutations of the parts of $\lambda$ after padding $\lambda$ with enough zeros to make a length-$r$ vector. If $\ell(\lambda)>r$, no such exponent vector exists. For every exponent vector $a$ with $\lambda(a)=\lambda$, the coefficient of the monomial \begin{align*} y_1^{a_1}\cdots y_r^{a_r} \end{align*} in the expansion of $\Omega_r$ is \begin{align*} h_{a_1}(x)\cdots h_{a_r}(x). \end{align*} Because the product in $\operatorname{Sym}$ is commutative and $h_0(x)=1$, rearranging the factors and deleting the factors $h_0(x)$ gives \begin{align*} h_{a_1}(x)\cdots h_{a_r}(x)=h_{\lambda_1}(x)\cdots h_{\lambda_{\ell(\lambda)}}(x)=h_\lambda(x). \end{align*} Thus all monomials whose exponent vector sorts to $\lambda$ have the same coefficient $h_\lambda(x)$. The sum of those monomials is exactly the finite-variable monomial symmetric function: \begin{align*} m_\lambda(y_1,\dots,y_r) = \sum_{\substack{a\in \mathbb{N}^r\\ \lambda(a)=\lambda}} y_1^{a_1}\cdots y_r^{a_r}. \end{align*} Therefore the full grouped expansion is \begin{align*} \Omega_r(x;y_1,\dots,y_r) = \sum_{\lambda} h_\lambda(x)m_\lambda(y_1,\dots,y_r), \end{align*} with the convention that $m_\lambda(y_1,\dots,y_r)=0$ when $\ell(\lambda)>r$. [/guided] [/step] [step:Pass from finite $y$-variable identities to the completed tensor product] Let \begin{align*} \pi_r:\widehat{\operatorname{Sym}}_y \to \mathbb{Z}[[y_1,\dots,y_r]] \end{align*} denote the specialization map setting $y_j=0$ for all $j>r$, extended continuously to the completion. The induced continuous map \begin{align*} \operatorname{id}\widehat{\otimes}\pi_r: \widehat{\operatorname{Sym}}_x\widehat{\otimes}\widehat{\operatorname{Sym}}_y \to \widehat{\operatorname{Sym}}_x[[y_1,\dots,y_r]] \end{align*} sends $\Omega(x,y)$ to $\Omega_r(x;y_1,\dots,y_r)$ and sends $m_\lambda(y)$ to $m_\lambda(y_1,\dots,y_r)$. By the finite-variable identity proved above, \begin{align*} (\operatorname{id}\widehat{\otimes}\pi_r)\Omega(x,y) = (\operatorname{id}\widehat{\otimes}\pi_r) \left(\sum_{\lambda} h_\lambda(x)m_\lambda(y)\right) \end{align*} for every $r\geq 1$. The completed symmetric functions in the $y$-variables are determined by all their finite-variable specializations, because each homogeneous component involves only finitely many monomial symmetric functions of a fixed degree and each such component is detected after taking $r$ at least the length of the indexing partitions. Hence the two elements of \begin{align*} \widehat{\operatorname{Sym}}_x\widehat{\otimes}\widehat{\operatorname{Sym}}_y \end{align*} are equal. Therefore \begin{align*} \Omega(x,y)=\sum_{\lambda}h_\lambda(x)m_\lambda(y), \end{align*} as claimed. [/step]