ac.commutative algebra - Finiteness of injective hull of residue field for Artin local ring

This is a proof of $ell(M)=ell(mbox{Hom}(M,mbox{E}(A/mathfrak{m}))$ suggested by Mariano:

Induction on $ell(M) $:

If $ell(M)=0$, $M=0$ so obviously true. Suppose $ell(M)=ngeq 1$. From a composition series of $M$ choose the submodule N right beneath M so that $ell(N)=n-1$ and $M/Nsimeq A/mathfrak{m}$. $0rightarrow Nrightarrow M rightarrow A/mathfrak{m}rightarrow 0$ induces $0leftarrow mbox{Hom}(N,E(A/mathfrak{m}))leftarrow mbox{Hom}(M,E(A/mathfrak{m}))leftarrow mbox{Hom}(A/mathfrak{m},E(A/mathfrak{m}))leftarrow 0$.

Now $mbox{Hom}(A/mathfrak{m},E(A/mathfrak{m}))simeq A/mathfrak{m}$ since $E(A/mathfrak{m})$ is an essential extension of $A/mathfrak{m}$, and $ell(mbox{Hom}(N,E(A/mathfrak{m})))=ell(N)=n-1$ by the induction hypothesis. $ell(A/mathfrak{m})=1$ so $ell(mbox{Hom}(M,E(A/mathfrak{m}))=(n-1)+1=n$