$K[[X_1,...]]$ is a UFD (Nishimura's Theorem) Let us define the infinitely-many-variable formal power series ring 
$$
K[[X_1,\ldots]] \colon= \underset{m \geq 1}{\varprojlim}\,K[[X_1,\ldots,X_m]].
$$
$K[[X_1,\ldots]]$ is known to be a UFD by a theorem of Nishimura (c.f. On the unique factorisation theorem for formal power series, Journal Math. Kyoto. Univ. Vol 7. No 2. 1967, 151-160). 
Now let us choose an irreducible element $f \in K[[X_1,\ldots]]$ and consider the image $f_m \in K[[X_1,\ldots,X_m]]$ of $f$ by the natural quotient ring homomorphism $K[[X_1,\ldots]] \twoheadrightarrow K[[X_1,\ldots,X_m]]$.  
Q. Is $f_m$ also irreducible for $m \gg 0$?
 A: Permit me to make the following bibliographic remark: the very same article of Nishimura which was cited by OP, already contains an affirmative answer to the OP's question: (1) on page 157 of Nishimura's 1967 article one reads 



Nishimura's proof, which seems self-contained and recommendable reading, uses too many preliminary results to be conveniently summarizable (by me). I tried to write an exposition, but that attempt foundered on my not understanding Nishiguro's argument in few places (which does imply anything for Nishimura's proof of course).
${}$___________________________
(1) So the OP either did not read or did not trust Nishigura's article in its entirety (and thought it more polite to not mention any issues that there may or may not be with Ishimura's argument); of course there isn't anything wrong with that; it's perfectly fine to quote Nishigura's article for the purpose of giving a reference for the UFD-claim only. I simply think it should be pointed out for completeness that Nishimura's article seems to already contain an answer. 
A: (I assume that $K$ is a field)
Decompose each $f_m$ into a product of irreducible series $f_m=g^1_m\dots g^{i_m}_m$. For each $m$ we get $f_m=\overline{g^{1}_{m+1}}\dots \overline{g^{i_{m+1}}_{m+1}}$ where overline denotes the reduction map $K[[x_1,\dots, x_m,x_{m+1}]]\to K[[x_1,\dots, x_m]]$. Since $K[[x_1,\dots,x_m]]$ is a UFD, $\overline{g^j_{m+1}}$ is a product of some elements $g^{k_1},\dots ,g^{k_{n_{j,m+1}}}$ up to a unit. More precisely, decompositions of $f_m$s give a sequence of partitions of the set $\{1,\dots, i_1\}$ such that the $m$-th partition is a refinement of the $(m+1)$-th for every $m$.
If there are no $N$ such that for every $m>N$ the series $f_m$ is irreducible, all these partitions consist of at least two elements. However, the sequence of positive integers $i_1\geq i_2\geq \dots$ must stabilize eventually, so there is a number $N$ such that for every $m\geq N$ we get (maybe after permuting the irreducible factors) $\overline{g^k_{m+1}}=g^k_mu^k_m$ where $u^k_m$ are units such that $u^1_{m}\dots u^{i_m}_{m}=1$. We will now modify the decompositions to obtain a decomposition of $f$. Namely for each $m\geq {N-1}$, put $h^k_{m+1}=g^{k}_{m+1}\cdot (\iota(u^k_N)\iota(u^{k}_{N+1})\dots \iota(u^{k}_{m}))^{-1}$ where $\iota^{m+1}_{l}:K[[x_1,\dots, x_l]]\to K[[x_1,\dots, x_{m+1}]]$ are the embeddings. 
We've arranged things so that $f_{m}=h^{1}_m\dots h^{i}_m$ for all $m\geq N$ ($i$ is the stabilizing value of the sequence $(i_m)$) and $\overline{h^k_{m+1}}=h^k_m$. Hence, we get non-invertible elements $h^k$ of $K[[x_1,\dots]]$ such that $f=h^1\dots h^i$ so $f$ is reducible.
A: I suppose the natural quotient ring homomorphism is the one that sets $X_k = 0$ for $k>m$.
For small $m$, I think that $X_1^2 - X_2^2 + X_3^2 \twoheadrightarrow (X_1 - X_2) (X_1 + X_2)$, with $m=2$, is a counter example. But for any $f \in K[[X_1,\ldots]]$ there is a sufficiently large $m$ such that $f \in K[[X_1,\ldots,X_m]]$ (by the structure of the inductive limit), so that $f_m = f$. But then, reducibility in $K[[X_1,\ldots,X_m]]$ trivially implies reducibility in $K[[X_1,\ldots]]$. The the answer to your Q seems to be Yes.
