Kac moody verma module has a unique simple quotient

A submodule $N$ is a sum of its weight intersections by F2. Explicitly, for a finite weight sum $x={\sum }_{j=1}^r{x}_{{\mu }_j}\in N$, choose $h\in \mathfrak{h}$ with all ${\mu }_j(h)$ distinct. Such an $h$ exists: in a finite basis $h_1,\dots ,h_d$, the curve $h(t)={\sum }_{a=1}^d{t}^{a-1}{h}_a$ makes each nonzero difference $({\mu }_j-{\mu }_l)(h(t))$ a nonzero polynomial, and finitely many such polynomials exclude only finitely many complex $t$. Applying ${\prod }_{l\mathrm{\ne }j}(h-{\mu }_l(h))\mathrm{/}({\mu }_j(h)-{\mu }_l(h))$ to $x$ gives $x_{{\mu }_j}\in N$. If $N$ has nonzero top space, it contains $v_{\lambda }$ because that space is one dimensional; since $v_{\lambda }$ generates $M_A(\lambda )$, then $N=M_A(\lambda )$.

Form the algebraic sum $N_{\lambda }$ of all proper submodules, meaning all finite sums of their elements. This is a submodule. Each summand has zero top component by 1.1, so every such finite sum has zero top component. Thus $N_{\lambda }$ is proper and contains every proper submodule. A strictly larger submodule must be the whole module, proving both maximality and uniqueness. Its quotient is nonzero since the top vector survives; any proper nonzero submodule of the quotient would lift to a submodule strictly between $N_{\lambda }$ and the whole module, which is impossible. The surviving top vector generates the quotient, so it is simple highest weight $\lambda$.

If a simple module $V$ has a specified nonzero highest vector of weight $\lambda$, F1 supplies a map $M_A(\lambda )\to V$ whose image is the cyclic submodule generated by that vector, hence all of $V$. Its kernel is maximal proper, because an intermediate submodule would give a nonzero proper submodule of $V$. By 2.1 this kernel is $N_{\lambda }$, giving the stated isomorphism. If $M_A(\lambda )$ itself is simple, the sum in 2.1 is just zero and the same construction applies. Finite interpolation includes the single-weight case with empty product $1$. No Zorn argument, arbitrary family of choices or finite-dimensionality of the whole module is used.