Write a = \alpha x, b = \beta y with \alpha,\beta \in \Gamma and x,y \in \sY_\infty. Since \Gamma and \sY_\infty are abelian and \Gamma acts on \sY_\infty through the \Lam-structure, a direct expansion of the commutator gives aba^{-1}b^{-1} = (x^{\alpha})^{1-\beta}\,(y^{\beta})^{\alpha-1}. Taking \beta = 1, \alpha = \gamma_0 shows (\gamma_0-1)\sY_\infty \subseteq G'. Conversely, writing \beta = \gamma_0^c with c \in \Zp, the binomial expansion 1 - \beta = -\sum_{n\ge 1}\binom{c}{n}(\gamma_0-1)^n \in T\Lam, and likewise \alpha - 1 \in T\Lam; so every commutator lies in T\,\sY_\infty.

Take n = 0. As \sL_0 is the maximal unramified abelian p-extension of F and \sL_\infty/F is a pro-p-extension, \sL_0/F is the maximal unramified abelian subextension of \sL_\infty. Thus \sY_0 = \Gal(\sL_0/F) is G modulo the subgroup generated by G' and the inertia I. Using Proposition 13.2.1.1 (G' = T\sY_\infty) and G = I\,\sY_\infty, \sY_0 = G/\langle G', I\rangle = \sY_\infty/(\gamma_0-1)\sY_\infty = \sY_\infty/T\,\sY_\infty. For n \ge 1 repeat with F replaced by F_n and \gamma_0 by \gamma_0^{p^n}; then (\gamma_0^{p^n}-1)\sY_\infty = ((1+T)^{p^n}-1)\sY_\infty = \varphi^n(T)\sY_\infty, giving the claim.

This is the topological Nakayama lemma for the complete local ring \Lam, whose maximal ideal is \mathfrak{m} = (p,T). If \sY is finitely generated then \sY/\mathfrak{m}\sY is a finite-dimensional vector space over the residue field \Lam/\mathfrak{m} = \Fp, hence finite. Conversely, suppose \sY/\mathfrak{m}\sY is finite, with classes of x_1,\dots,x_m spanning it. Let M \subseteq \sY be the closed \Lam-submodule they generate. Then \sY = M + \mathfrak{m}\sY, so iterating, \sY = M + \mathfrak{m}^k\sY for every k. Because \sY is compact and \bigcap_k \mathfrak{m}^k\sY = 0 (the \mathfrak{m}-adic topology is Hausdorff on the compact module), any y \in \sY is a limit of elements of M modulo \mathfrak{m}^k; completeness of \Lam lets the correcting coefficients converge, placing y \in M. Thus \sY = M is finitely generated. The same argument with \sY/\mathfrak{m}\sY = 0 gives \sY = \mathfrak{m}\sY = 0.

Since \varphi(T) = (1+T)^p - 1 = \sum_{k=1}^p \binom{p}{k} T^k \in (p,T), the quotient \sY_\infty/(p,T)\sY_\infty is a quotient of \sY_\infty/\varphi(T)\sY_\infty = \sY_1 = \Cl(F_1)\otimes\Zp by Proposition 13.2.1.2, which is finite. By Lemma 13.2.1.3, \sY_\infty is finitely generated over \Lam.

Place the two short exact sequences 0 \to \varphi^n(T)\sY_\infty \to \sY_\infty \to \sY_\infty/\varphi^n(T) \to 0 and the analogous one for \sA in a commutative ladder, with vertical maps induced by the quasi-isomorphism \sY_\infty \to \sA of finite kernel Q and cokernel R. The middle vertical map has kernel Q and cokernel R, both of order bounded uniformly in n. Applying the snake lemma to the squares gives, for the third vertical map \sY_\infty/\varphi^n(T) \to \sA/\varphi^n(T), kernels and cokernels that are sub- and sub-quotients of Q, R and the snake connecting maps. As Q, R are finite, these are uniformly bounded; one checks they moreover stabilise for n \ge n_0 (the connecting maps eventually no longer change because \varphi^n(T) annihilates Q and R once n is large). Comparing orders across the third column, \abs{\sY_\infty/\varphi^n(T)} and \abs{\sA/\varphi^n(T)} differ by the fixed factor p^c.

Step 1 (r=0). The polynomial \varphi^n(T) = T^{p^n} + \sum_{k=1}^{p^n-1}\binom{p^n}{k}T^k is distinguished. By Weierstrass division (a p-adic Euclidean algorithm) every f \in \Zp[[T]] is uniquely q(T)\varphi^n(T) + r(T) with \deg r \le p^n-1, so \Lam/\varphi^n(T) \cong \{r(T) \in \Zp[T] : \deg r \le p^n-1\} is infinite. As \sA/\varphi^n(T) is finite, the free part must vanish: r = 0.

Step 2 (the \Lam/(p^{m_i}) summands). Reducing the displayed isomorphism mod p^k, \Lam/(p^k,\varphi^n(T)) is the space of degree \le p^n-1 polynomials over \Z/p^k\Z, so has order p^{k p^n}. Summing, the second part of \sA contributes p^{m p^n}, with m = \sum_i m_i.

Step 3 (the \Lam/(f_j^{k_j}) summands). Let g be distinguished of degree d and V = \Lam/(g). By Lemma 13.2.2.3, for n large \varphi^{n+1}(T)V = p\,\varphi^n(T)V. Since (p,g)-coprimality makes multiplication by p injective on V, and \abs{V/pV} = \abs{\Lam/(p,T^d)} = p^d, an induction gives \abs{V/\varphi^{n+1}(T)V} = p^{d}\,\abs{V/\varphi^n(T)V}, hence \abs{V/\varphi^n(T)V} = p^{nd + c}. Applying with g = f_j^{k_j} and summing, the third part contributes p^{\ell n + c}, \ell = \sum_j k_j\deg f_j. Multiplying the three contributions proves the formula.

As g is distinguished, T^k \equiv p\cdot(\text{poly}) \pmod{g} for all k \ge d. For k \ge n_0 we have p^k \ge d, so \varphi^k(T) = T^{p^k} + p\,(\text{poly}) \equiv p\,Q_k(T) \pmod g. From the factorisation X^{p^{k+1}}-1 = (X^{p^k}-1)\big(X^{p^k(p-1)} + \cdots + 1\big) with X = 1+T, \varphi^{k+1}(T) \equiv \varphi^{k}(T)\Big[(pQ_k+1)^{p-1} + \cdots + (pQ_k+1) + 1\Big] \pmod g. Every term in the bracket is divisible by p except the p constant terms, which sum to p; hence \varphi^{k+1}(T) \equiv p\,\varphi^k(T) \pmod g. Taking k = n_0 forces Q_{n_0+1} \equiv 0 \pmod p, and inductively Q_n \equiv 0 \pmod p for all n > n_0. Re-running the computation with k = n > n_0: now each binomial term is divisible by p^2 except the constant terms summing to p, so \varphi^{n+1}(T) \equiv p\,\varphi^n(T)\big[p\cdot(\text{poly}) + 1\big] \pmod g, and p\cdot(\text{poly})+1 is a unit in V. Therefore \varphi^{n+1}(T)V = p\,\varphi^n(T)V.

By Proposition 13.2.2.2, finiteness of all \sA/\varphi^n(T) forces r = 0 in the structure theorem, so the standard module \sA is torsion — every element is annihilated by its characteristic ideal Definition 12.1.4. As \sY is quasi-isomorphic to such an \sA (finite kernel and cokernel) and torsionness is preserved under quasi-isomorphism, \sY is torsion.