Every comodule element lies in a finite-dimensional subcomodule

If $m=0$, let $W=\{0\}$ with its zero coaction; both coaction equations are zero equalities, so it is a finite-dimensional subcomodule containing $m$. Otherwise write $\rho (m)={\sum }_{s=1}^r{x}_s\otimes d_s$ as a finite tensor by [F2]. Let $D=\mathrm{span}\{d_1,\dots ,d_r\}$. The choice-free basis-extraction result [F5] gives a finite basis $c_1,\dots ,c_q$ of $D$; express each $d_s$ in that basis and collect terms to obtain $\rho (m)={\sum }_{i=1}^q{v}_i\otimes c_i$ with the $c_i$ linearly independent. Set $W=\mathrm{span}\{v_1,\dots ,v_q\}$, which has a finite basis and is therefore finite-dimensional by [F5].

Coassociativity applied to this expansion gives ${\sum }_i\rho (v_i)\otimes c_i={\sum }_i{v}_i\otimes \mathrm{\Delta }(c_i)$. Let $\pi :M\to M\mathrm{/}W$ be the quotient and apply $\pi \otimes {\mathrm{id}}_C\otimes {\mathrm{id}}_C$; the right side is zero since every $v_i\in W$, so ${\sum }_i((\pi \otimes {\mathrm{id}}_C)\rho (v_i))\otimes c_i=0$ in $((M\mathrm{/}W)\otimes C)\otimes C$.

Apply the associator and symmetry to rewrite the last equality as ${\sum }_i{c}_i\otimes ((\pi \otimes \mathrm{id})\rho (v_i))=0$. The $c_i$ are independent, so [F3] gives $(\pi \otimes \mathrm{id})\rho (v_i)=0$ for every $i$. By [F4], each $\rho (v_i)$ lies in the image of $W\otimes C\to M\otimes C$. Therefore $\rho (W)$ lies in that image.

Now suppose $C$ is finite-dimensional, without assuming AC. The construction in step 1.1 still gives $W$ and independent $c_i$. Coassociativity and the quotient map give the zero tensor equality of step 2.1. The finite-dimensional clause of [F3] therefore gives $(\pi \otimes \mathrm{id})\rho (v_i)=0$ for each $i$.

The inclusion $i:W\hookrightarrow M$ tensored with $C$ is injective by [A1] and [F4]. Hence each $\rho (w)$ for $w\in W$ has a unique lift ${\rho }_W(w)\in W\otimes C$; uniqueness makes $w\mapsto {\rho }_W(w)$ linear and $(i\otimes \mathrm{id}){\rho }_W=\rho i$. The map $i\otimes {\mathrm{id}}_C\otimes {\mathrm{id}}_C$ is also injective. Applying it to $({\rho }_W\otimes \mathrm{id}){\rho }_W$ gives $(\rho \otimes \mathrm{id})(i\otimes \mathrm{id}){\rho }_W=(\rho \otimes \mathrm{id})\rho i$; applying it to $({\mathrm{id}}_W\otimes \mathrm{\Delta }){\rho }_W$ gives $({\mathrm{id}}_M\otimes \mathrm{\Delta })(i\otimes \mathrm{id}){\rho }_W=({\mathrm{id}}_M\otimes \mathrm{\Delta })\rho i$. These are equal by coassociativity of $M$, so injectivity proves coassociativity on $W$. Also $i({\mathrm{id}}_W\otimes \epsilon ){\rho }_W=({\mathrm{id}}_M\otimes \epsilon )(i\otimes \mathrm{id}){\rho }_W=({\mathrm{id}}_M\otimes \epsilon )\rho i=i$; injectivity of $i$ proves counitality. Thus $(W,{\rho }_W)$ is a finite-dimensional subcomodule. Finally $m=({\mathrm{id}}_M\otimes \epsilon )\rho (m)={\sum }_i{v}_i\epsilon (c_i)\in W$ by [F1].

Since $C$ is finite-dimensional, [F5] and Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis give a finite basis $d_1,\dots ,d_t$ of $C$. Write ${\lambda }_s(c)$ for the unique $s$th coordinate of $c\in C$ from [F6]. For $a,b\in k$ and $c,c^{\mathrm{\prime }}\in C$, uniqueness of coordinates and the vector-space laws give ${\lambda }_s(ac+b{c}^{\mathrm{\prime }})=a{\lambda }_s(c)+b{\lambda }_s(c^{\mathrm{\prime }})$, so each ${\lambda }_s$ is linear; write $d_s^{\ast }:={\lambda }_s$. Write $\rho (v_i)={\sum }_s{y}_s\otimes d_s$. Applying $\pi \otimes \mathrm{id}$ and then $\mathrm{id}\otimes d_s^{\ast }$ gives $\pi (y_s)=0$, hence each $y_s\in W$; so $\rho (v_i)$ is in the image of $W\otimes C$. The inclusion $W\otimes C\to M\otimes C$ is injective without AC here: if ${\sum }_s{w}_s\otimes d_s$ maps to zero, applying ${\mathrm{id}}_M\otimes d_s^{\ast }$ gives $w_s=0$ for each $s$. Thus the coaction lifts uniquely and linearly to $W$. Writing $i:W\hookrightarrow M$ for the inclusion, expand each elementary tensor in the two finite $C$-coordinates to write any $z\in W\otimes C\otimes C$ as $z={\sum }_{s,u}{w}_{su}\otimes d_s\otimes d_u$ by [F2]. If its image in $M\otimes C\otimes C$ is zero, apply ${\mathrm{id}}_M\otimes d_s^{\ast }\otimes d_u^{\ast }$, with the canonical tensor-unit identifications, to obtain $i(w_{su})=0$ for every $s,u$; injectivity of $i$ gives $w_{su}=0$ and hence $z=0$. Thus the threefold inclusion is injective without invoking a product-basis theorem or AC. Applying this inclusion to the two coaction composites on $W$ gives the corresponding composites on $M$, which agree by coassociativity; hence coassociativity holds on $W$. Likewise, applying $W\hookrightarrow M$ to its counit composite gives the identity on $W$ by counitality on $M$, and injectivity gives counitality on $W$. Finally, step 2.1 and counitality directly give $m=({\mathrm{id}}_M\otimes \epsilon )\rho (m)={\sum }_i{v}_i\epsilon (c_i)\in W$.

Steps 1.1, 2.1, 3.1, and 4.1 prove the arbitrary-$C$ case under AC; steps 2.1, 3.2, and 4.2 prove the finite-dimensional-$C$ case without AC. In both cases the exhibited $W$ is finite-dimensional and is a subcomodule containing $m$.