$K[[X]]$ is not a finitely generated $K[X]$-module. 
How can I  prove that $K[[X]]$ is not finitely generated over $K[X]$ as a module, where $K$ is a field.

What I tried: if above is not true then $K[[X]]$ is integral extension over $K[X]$. But I failed to draw any contradiction. 
Help me. Thanks
 A: Inspired by the counting suggested by Hagen, here is a proof that shows $K[[X]]$ is not even of finite type over $K[X]$.
First, note that this holds when $K$ is at most countable, for in this case $K[X]$ is countable while $K[[X]]$ is uncountable, and any ring of finite type over a countable ring is still countable.
Now the general case. Suppose $K[[X]]=K[X,f_1,\dots,f_n]$. Let $k$ be the field generated by the prime field of $K$ (namely $\mathbb Q$ or $\mathbb F_p$) and the (countably many) coefficients of $f_i$. Then $k$ is countable. By the above argument, $k[[X]]$ is not of finite type over $k[X]$, so there is $g\in k[[X]]$ such that $g\notin k[X,f_1,\dots,f_n]$. This means that, for any $N\in\mathbb N$, the equation
$$ g=\sum_{\alpha_i\le N\atop\deg p_\alpha\le N} p_\alpha f_1^{\alpha_1}\cdots f_n^{\alpha_n} \tag{*}$$
has no solution $p_{\alpha}\in k[X]$. This can be thought of an (infinite) system of linear equations in the finitely many (in fact $(N+1)^{n+1})$ coefficients of $p_\alpha$, whose own coefficients lie in $k$. Since it has no nonzero solution in $k$, finitely many of the equations already has no nonzero solution in $k$. Since the existence of nonzero solutions to a system of linear equations does not depend on the ground field, the same finitely many equations has no nonzero solution in the larger field $K$, and hence the system as a whole has no nonzero solution $K$. This implies that (*) is not satisfiable either in $K$. Since this is true for any $N\in\mathbb N$, $g\notin K[X,f_1,\dots,f_n]$.
A: An alternative approach showing that $K[[X]]$ is not a finitely generated $K$-algebra, and hence not a finitely generated $K[X]$-algebra. 

If a finitely generated algebra over a field is a local ring then it is artinian.

Suppose that $K[X_1,\dots,X_n]/I$ is a local ring, for some ideal $I$. Then $I$ is contained in a single maximal ideal, say $M$, so $\sqrt I=M$ (since a polynomial ring over a field is a Jacobson ring). In particular, $\dim K[X_1,\dots,X_n]/I=0$, and thus $K[X_1,\dots,X_n]/I$ is an artinian local ring. 
A: The inclusion of rings $j:K[X] \hookrightarrow K[[X]]$ induces a map $j^\ast: \operatorname {Spec}(K[[X]])\to \operatorname {Spec}(K[X])$ between the corresponding sets of prime ideals of these rings.
If  $K[[X]]$ were module-finite (or even just integral) over $K[X]$, the  map  $j^\ast: \operatorname {Spec}(K[[X]])\to \operatorname {Spec}(K[X])$ would be surjective: Atiyah-Macdonald, Theorem 5.10 .
But this is impossible since $K[[X]]$ (like all discrete valuation rings) has only two prime ideals, whereas $K[X]$ has infinitely many (by a variation of Euclid's proof of the infinitude of prime integers).
A: In the following context we assume everything is commutative.

Definition: A Jacobson ring is a ring where every prime ideal is an intersection of some maximal ideals.

Then we have the fact (cf. Eisenbud Commutative Algebra with a View towards Algebraic Geometry Theorem 4.19) that:

Fact (Nullstellensatz): Let $A$ be a Jacobson ring, then any finitely generated $A$-algebra is a Jacobson ring.

Now apply this result to the question. 
First note that a field $K$ is obviously a Jacobson ring, by Nullstellensatz $K[X]$ is a Jacobson ring. Next note that if a local ring has more than one prime ideal, then it cannot be a Jacobson ring. Now $K[[X]]$ is a local ring with prime ideals $(X)$ and $(0)$, hence it cannot be a Jacobson ring. Hence it cannot be a finitely generated $K[X]$-algebra. (A fortiori not finite $K[X]$-module.)
A: In $K[[X]]$, the element $f=\sum_{i=0}^\infty X^i$ is an inverse of $1-X$. Since $K[X]$ is integrally closed (even a PID), $(1-X)^{-1}$ can't be integral over $K[X]$. Therefore  $K[X][f] \subseteq K[[X]]$ is a not f.g submodule. Since $K[X]$ is Noetherian (by Hilbert Basis Theorem), we can conclude that $K[[X]]$ can't be finitely generated either.
