[proofplan]
Choose one nonzero vector in each negative root space and order the positive roots. The PBW model of the Verma module identifies $M(\lambda)$ with $U(\mathfrak n^-)$ applied to the highest weight vector, so ordered PBW monomials in the negative root vectors form a basis. Each occurrence of the root vector from $\mathfrak g_{-\alpha}$ lowers the $\mathfrak h$-weight by $\alpha$, and summing these basis weights gives a product of geometric series. Finally, finiteness of the positive root system guarantees that every coefficient in the completed formal character is finite.
[/proofplan]
[step:Choose ordered negative root vectors for the PBW basis]
Since $\mathfrak g$ is complex semisimple, each root space $\mathfrak g_\alpha$ is one-dimensional. Fix a total order
\begin{align*}
\Phi^+=\{\alpha_1,\dots,\alpha_N\}
\end{align*}
on the finite set of positive roots, where $N:=|\Phi^+|$. For each index $i\in\{1,\dots,N\}$, choose a nonzero vector
\begin{align*}
f_i\in\mathfrak g_{-\alpha_i}.
\end{align*}
Then $(f_1,\dots,f_N)$ is an ordered basis of
\begin{align*}
\mathfrak n^-=\bigoplus_{\alpha\in\Phi^+}\mathfrak g_{-\alpha}.
\end{align*}
Let $v_\lambda:=1\otimes 1\in M(\lambda)$ denote the canonical highest weight vector. The hypotheses of the [PBW model of a Verma module](/theorems/9374) [citetheorem:9374] are satisfied by the fixed triangular decomposition, the Borel subalgebra $\mathfrak b=\mathfrak h\oplus\mathfrak n^+$, and the one-dimensional $\mathfrak b$-module $\mathbb C_\lambda$ from the statement. Therefore the vectors $f_1^{m_1}f_2^{m_2}\cdots f_N^{m_N}v_\lambda$, with $(m_1,\dots,m_N)\in\mathbb Z_{\ge 0}^N$, form a complex basis of $M(\lambda)$.
[/step]
[step:Compute the weight of each PBW monomial]
For each $i\in\{1,\dots,N\}$ and each $h\in\mathfrak h$, the defining property $f_i\in\mathfrak g_{-\alpha_i}$ gives
\begin{align*}
[h,f_i]=-\alpha_i(h)f_i.
\end{align*}
Let $m=(m_1,\dots,m_N)\in\mathbb Z_{\ge 0}^N$, and define the PBW vector
\begin{align*}
v_m:=f_1^{m_1}f_2^{m_2}\cdots f_N^{m_N}v_\lambda\in M(\lambda).
\end{align*}
We prove that $v_m$ has $\mathfrak h$-weight
\begin{align*}
\lambda-\sum_{i=1}^N m_i\alpha_i.
\end{align*}
Indeed, commuting $h$ past the ordered product $f_1^{m_1}\cdots f_N^{m_N}$ and using $h v_\lambda=\lambda(h)v_\lambda$ gives
\begin{align*}
h v_m=\left(\lambda(h)-\sum_{i=1}^N m_i\alpha_i(h)\right)v_m.
\end{align*}
Since this holds for every $h\in\mathfrak h$, the asserted weight formula follows.
[guided]
The key point is that each negative root vector is an eigenvector for the adjoint action of $\mathfrak h$. For every $i\in\{1,\dots,N\}$, the condition $f_i\in\mathfrak g_{-\alpha_i}$ means precisely that, for every $h\in\mathfrak h$,
\begin{align*}
[h,f_i]=-\alpha_i(h)f_i.
\end{align*}
Equivalently,
\begin{align*}
h f_i=f_i h-\alpha_i(h)f_i
\end{align*}
inside the enveloping algebra action on $M(\lambda)$.
Let $m=(m_1,\dots,m_N)\in\mathbb Z_{\ge 0}^N$, and set
\begin{align*}
v_m:=f_1^{m_1}f_2^{m_2}\cdots f_N^{m_N}v_\lambda.
\end{align*}
When $h$ acts on $v_m$, commute $h$ to the right across the product $f_1^{m_1}\cdots f_N^{m_N}$. Each time $h$ crosses one copy of $f_i$, the scalar contribution is $-\alpha_i(h)$. Since there are $m_i$ copies of $f_i$, the total contribution from the $i$th root vector is $-m_i\alpha_i(h)$. After $h$ reaches the highest weight vector, the defining action on $\mathbb C_\lambda$ gives
\begin{align*}
h v_\lambda=\lambda(h)v_\lambda.
\end{align*}
Combining these scalar contributions yields
\begin{align*}
h v_m=\left(\lambda(h)-\sum_{i=1}^N m_i\alpha_i(h)\right)v_m.
\end{align*}
This identity holds for every $h\in\mathfrak h$, so $v_m$ lies in the weight space of weight
\begin{align*}
\lambda-\sum_{i=1}^N m_i\alpha_i.
\end{align*}
[/guided]
[/step]
[step:Identify the weight multiplicities with coefficient counts]
For $\beta\in Q_+$, define
\begin{align*}
c_\beta:=\#\left\{(m_1,\dots,m_N)\in\mathbb Z_{\ge 0}^N:\sum_{i=1}^N m_i\alpha_i=\beta\right\}.
\end{align*}
The PBW basis from the first step and the weight computation from the second step imply
\begin{align*}
\dim M(\lambda)_{\lambda-\beta}=c_\beta.
\end{align*}
If $\mu\notin\lambda-Q_+$, then $M(\lambda)_\mu=0$.
It remains to note that $c_\beta$ is finite. Let $\Delta\subset\Phi^+$ be the simple root system. Define the height map
\begin{align*}
\operatorname{ht}:Q_+\to\mathbb Z_{\ge 0}
\end{align*}
by declaring that, for each element $\gamma=\sum_{\delta\in\Delta}a_\delta\delta\in Q_+$ written in the simple-root basis,
\begin{align*}
\operatorname{ht}(\gamma):=\sum_{\delta\in\Delta}a_\delta.
\end{align*}
Each positive root has height at least $1$. Therefore every tuple counted by $c_\beta$ satisfies
\begin{align*}
\sum_{i=1}^N m_i\le \operatorname{ht}(\beta).
\end{align*}
There are only finitely many nonnegative integer tuples with this bound, so $c_\beta<\infty$.
[/step]
[step:Sum the PBW weights as a product of geometric series]
By the character convention in the statement, the formal character of $M(\lambda)$ is the completed group-algebra sum
\begin{align*}
\operatorname{ch}M(\lambda)=\sum_{\mu}\dim M(\lambda)_\mu e^\mu,
\end{align*}
where the sum ranges over weights with nonzero weight space. Using the [multiplicity formula](/theorems/2420) from the previous step, this becomes
\begin{align*}
\operatorname{ch}M(\lambda)=\sum_{(m_1,\dots,m_N)\in\mathbb Z_{\ge 0}^N} e^{\lambda-\sum_{i=1}^N m_i\alpha_i}.
\end{align*}
Factoring out $e^\lambda$ and separating the independent nonnegative exponents gives
\begin{align*}
\operatorname{ch}M(\lambda)=e^\lambda\prod_{i=1}^N\left(\sum_{m_i=0}^{\infty}e^{-m_i\alpha_i}\right).
\end{align*}
In the completed group algebra supported in $\lambda-Q_+$, each factor is the formal geometric series
\begin{align*}
\sum_{m_i=0}^{\infty}e^{-m_i\alpha_i}=(1-e^{-\alpha_i})^{-1}.
\end{align*}
Thus
\begin{align*}
\operatorname{ch}M(\lambda)=e^\lambda\prod_{i=1}^N(1-e^{-\alpha_i})^{-1}=e^\lambda\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}.
\end{align*}
The coefficient of each $e^{\lambda-\beta}$ is finite by the preceding step, so the equality is meaningful in the stated completion. This proves the formula.
[/step]
