Dong's lemma: if $A(z),B(z),C(z)\in \operatorname{End}(V)[[z^{\pm 1}]]$ pairwise local, then $:\mathrel{A(z)B(z)}:$ and $C(z)$ are local.
I'm trying the following approach for proving the lemma:
We have the following characterization for formal power series that "vanish outside diagnal": if $(z-w)^k\sum_{n,m} f_{n,m}z^{-n-1}w^{-m-1}=0$ for some $k$, then $f_{i,n-i}$ is a polynomial of i when we fix $n$ and vary $i$.
Denote $[A(z),B(w)]=\sum_{i,n} P_{A,B}(i;n)z^{-i-1} w^{-(n-i)-1}$, in which $P_{A,B}(i;n)$ is a polynomial of $i$ when we fix $n$, namely $P_{A,B}(i;n)=[A_i,B_{n-i}]$. $P_{B,C}$ and $P_{A,C}$ defined similarity.
Now $$[:\mathrel{A(z)B(z)}:,C(w)]=\sum_{n,m} [(\sum_{i<0}A_iB_{n-i}+\sum_{i\ge 0}B_{n-i}A_i),C_m]z^{-n-2}w^{-m-1}$$.
Then $$[(\sum_{i<0}A_iB_{n-i}+\sum_{i\ge 0}B_{n-i}A_i),C_m]\\=\sum_{i<0}A_iP_{B,C}(n-i;n+m-i)+\sum_{i<0}P_{A,C}(i;m+i)B_{n-i}+\sum_{i\ge 0}B_{n-i}P_{A,C}(i;m+i)+\sum_{i<0}P_{B,C}(n-i;n+m-i)A_i$$.
A simple example is Heisenberg algebra: let $A,B,C$ all be $b(z)$. in this case $P(i;n)=\delta_n id$. Inspired by this example one would guess that $\sum_{i<0}P_{A,C}(i;m+i)B_{n-i}+\sum_{i\ge 0}B_{n-i}P_{A,C}(i;m+i)$ is a polynomial of $m$ when we fix $n+m$ and the same for rest two terms. But I can see how to do this, are there any hints?