Verma composition multiplicities are finite

The Verma module $M(\lambda )$ belongs to $\mathcal{O}$ and its center acts by the scalar character ${\chi }_{\lambda }$, so it belongs to ${\mathcal{O}}_{{\chi }_{\lambda }}$. A simple factor $L(\mu )$ can occur only when $\mu$ is a weight below $\lambda$ and ${\chi }_{\mu }={\chi }_{\lambda }$, hence under the stated Choice premise $\mu \in W\cdot \lambda$. The Weyl group is finite; no Casimir bound is needed for this finite list.

The finite weight-space detector bounds the number of strict inclusions in any submodule chain of $M(\lambda )$. Choose a finite chain of maximum possible length among these bounded integer lengths. If one factor were not simple, an intermediate submodule would refine it, contradicting maximality; thus this is a composition series. Taking a fixed weight is exact on these weight-module subquotients. Each occurrence of $L(\mu )$ contributes its one-dimensional highest-weight space in degree $\mu$; other factors contribute a nonnegative dimension. Thus $[M(\lambda ):L(\mu )]\le \dim M(\lambda {)}_{\mu }<\mathrm{\infty }$.