If we view the ring of formal power series $F[[x]]$ as a vector space over $F$, and we view the polynomial ring $F[x]$ as a subspace of $F[[x]]$, then the axioms of choice implies that $$F[[x]]=F[x]\oplus W$$ for some subspace $W$ of $F[[x]]$; we just need to extend $\{1,x,x^2,...\}$ into an (uncountable) Hamel basis for $F[[x]]$, and then take the span of the other basis elements.
My question is, is the existence of $W$ provable in $ZF$, or do we require the Axiom of Choice? And if it is provable without Choice, can we explicitly construct such a $W$?
Even for $F=\mathbb{Z}/2\mathbb{Z}$ this is not provable in $\mathsf{ZF}$. Note that the formal power series language is unnecessarily complicated, given that we're just thinking about vector spaces; really we just have $A=\bigoplus_{i\in\mathbb{N}}F$ sitting inside $B=\prod_{i\in\mathbb{N}}F$ in the obvious way and we're looking for a way to write $B=A\oplus W$ for some $W$.
A key point here is that $B$ is extremely "flexible" compared to $A$: if we pass to a symmetric extension $V'\supset V$ of the universe we have $A^{V'}=A$ but $B^{V'}\not=B$ in general.
In particular, fix any field $F\in V$ and consider forcing with finite sequences of elements of $F$ (intuitively we're building a Cohen-generic element of $B$) and look at the finite supports symmetric submodel corresponding to this forcing. If memory serves, in this model we wind up killing off any possible summand $W$, although the details are a bit annoying to check.