[proofplan] We first decompose the [tensor product](/page/Tensor%20Product) into irreducible finite-dimensional highest-weight modules using complete reducibility and the classification by dominant integral weights. We then apply the multiplicativity of characters on tensor products and additivity on finite direct sums to obtain the displayed expansion with the same coefficients. Finally, we prove uniqueness by showing that the irreducible characters $\operatorname{ch}L(\nu)$ are linearly independent in $\mathbb Z[P]$, using the highest-weight term $e^\nu$ and the dominance order. [/proofplan] [step:Decompose the tensor product into irreducible highest weight summands] Fix $\lambda,\mu\in P^+$. Since $L(\lambda)$ and $L(\mu)$ are finite-dimensional $\mathfrak g$-modules, their tensor product $L(\lambda)\otimes L(\mu)$ is finite-dimensional. By [Weyl's complete reducibility theorem](/theorems/3755) for finite-dimensional modules over complex semisimple Lie algebras, this tensor product is a finite [direct sum](/page/Direct%20Sum) of irreducible finite-dimensional $\mathfrak g$-modules; the hypotheses are satisfied because $\mathfrak g$ is complex semisimple and $L(\lambda)\otimes L(\mu)$ is finite-dimensional. By the [classification of finite-dimensional irreducible highest weight modules](/theorems/9373) [citetheorem:9373], every irreducible finite-dimensional summand is isomorphic to $L(\nu)$ for a unique $\nu\in P^+$. Therefore there are uniquely defined nonnegative integers $c_{\lambda,\mu,\nu}$, all but finitely many equal to $0$, such that \begin{align*} L(\lambda)\otimes L(\mu)\cong \bigoplus_{\nu\in P^+} L(\nu)^{\oplus c_{\lambda,\mu,\nu}}. \end{align*} [/step] [step:Convert the irreducible decomposition into a character expansion] Characters of finite-dimensional weight modules are additive on finite direct sums, and by the tensor product character formula [citetheorem:9387] they are multiplicative on tensor products. Applying these two properties to the decomposition from the previous step gives \begin{align*} \operatorname{ch}\bigl(L(\lambda)\otimes L(\mu)\bigr)=\sum_{\nu\in P^+}c_{\lambda,\mu,\nu}\operatorname{ch}L(\nu). \end{align*} By [citetheorem:9387] again, \begin{align*} \operatorname{ch}\bigl(L(\lambda)\otimes L(\mu)\bigr)=\operatorname{ch}L(\lambda)\operatorname{ch}L(\mu). \end{align*} Combining the two displayed equalities yields \begin{align*} \operatorname{ch}L(\lambda)\operatorname{ch}L(\mu)=\sum_{\nu\in P^+}c_{\lambda,\mu,\nu}\operatorname{ch}L(\nu). \end{align*} [/step] [step:Prove linear independence of irreducible finite-dimensional characters] Let $\Delta\subset\Phi^+$ denote the simple root system. We use the dominance order on $\mathfrak h^*$ defined by $\alpha\le\beta$ if and only if $\beta-\alpha$ is a nonnegative integral linear combination of elements of $\Delta$. For each $\gamma\in P$, let $e^\gamma\in\mathbb Z[P]$ denote the canonical group-algebra basis element indexed by $\gamma$. We prove that the family $\{\operatorname{ch}L(\nu):\nu\in P^+\}$ is linearly independent in $\mathbb Z[P]$. Let $F\subset P^+$ be a finite set and suppose integers $a_\nu\in\mathbb Z$ satisfy \begin{align*} \sum_{\nu\in F}a_\nu\operatorname{ch}L(\nu)=0. \end{align*} Assume, toward a contradiction, that some $a_\nu$ is nonzero. Choose $\nu_0\in F$ maximal in the dominance order among those $\nu\in F$ with $a_\nu\ne 0$. The irreducible highest weight module $L(\nu_0)$ has highest weight $\nu_0$, so the coefficient of $e^{\nu_0}$ in $\operatorname{ch}L(\nu_0)$ is $1$. If $\eta\in F$ and $\eta\ne\nu_0$, then the term $a_\eta\operatorname{ch}L(\eta)$ contributes $0$ to the coefficient of $e^{\nu_0}$. Indeed, if $a_\eta=0$, this is immediate. If $a_\eta\ne 0$ and $\nu_0$ were a weight of $L(\eta)$, then the highest-weight property would give $\nu_0\le\eta$ in the dominance order. Since $\eta\ne\nu_0$, this would contradict the maximality of $\nu_0$ among the weights in $F$ with nonzero coefficient. Hence $\nu_0$ is not a weight of $L(\eta)$ whenever $\eta\ne\nu_0$ and $a_\eta\ne0$. Taking the coefficient of $e^{\nu_0}$ in the relation gives \begin{align*} a_{\nu_0}=0, \end{align*} contradicting the choice of $\nu_0$. Hence every $a_\nu$ is zero, and the irreducible finite-dimensional characters are linearly independent. [guided] We need uniqueness of the coefficients in the character expansion, so we first isolate the algebraic fact that irreducible characters cannot satisfy a nontrivial finite integer relation. Let $\Delta\subset\Phi^+$ be the simple root system, and define the dominance order on $\mathfrak h^*$ by declaring $\alpha\le\beta$ exactly when $\beta-\alpha$ is a nonnegative integral linear combination of simple roots in $\Delta$. Also, for each $\gamma\in P$, write $e^\gamma$ for the canonical basis element of the integral group algebra $\mathbb Z[P]$ indexed by $\gamma$. Let $F\subset P^+$ be a finite set, and suppose that integers $a_\nu\in\mathbb Z$ satisfy \begin{align*} \sum_{\nu\in F}a_\nu\operatorname{ch}L(\nu)=0. \end{align*} We must prove that each $a_\nu$ is zero. Assume that at least one coefficient is nonzero. Among the finitely many dominant weights $\nu\in F$ with $a_\nu\ne 0$, choose a maximal one in the dominance order, and denote it by $\nu_0$. This choice is possible because the set of nonzero coefficients is finite. The key point is that $\operatorname{ch}L(\nu_0)$ contains the formal exponential $e^{\nu_0}$ with coefficient $1$. Indeed, $L(\nu_0)$ is a highest weight module of highest weight $\nu_0$, and its highest weight space is one-dimensional. Thus the coefficient of $e^{\nu_0}$ in $\operatorname{ch}L(\nu_0)$ is $1$. Now consider another summand $\operatorname{ch}L(\eta)$ with $\eta\in F$ and $\eta\ne\nu_0$. If $e^{\nu_0}$ occurs in $\operatorname{ch}L(\eta)$, then $\nu_0$ is a weight of the highest weight module $L(\eta)$, so $\nu_0\le \eta$ in the dominance order. But $\nu_0$ was chosen maximal among the weights with nonzero coefficient. Therefore any such $\eta$ with $a_\eta\ne 0$ cannot strictly dominate $\nu_0$. Since $\eta\ne\nu_0$, this means no nonzero-coefficient summand other than $L(\nu_0)$ contributes to the coefficient of $e^{\nu_0}$. Taking the coefficient of $e^{\nu_0}$ in the assumed relation therefore gives \begin{align*} a_{\nu_0}=0. \end{align*} This contradicts the defining choice of $\nu_0$ as a weight with $a_{\nu_0}\ne 0$. Hence the assumption of a nontrivial relation was false, and every coefficient $a_\nu$ is zero. The characters $\operatorname{ch}L(\nu)$ are linearly independent. [/guided] [/step] [step:Conclude that the character identity determines the tensor product multiplicities] Suppose another finite family of integers $d_\nu\in\mathbb Z$ satisfies \begin{align*} \operatorname{ch}L(\lambda)\operatorname{ch}L(\mu)=\sum_{\nu\in P^+}d_\nu\operatorname{ch}L(\nu). \end{align*} Subtracting this identity from the expansion obtained from the tensor product decomposition gives \begin{align*} \sum_{\nu\in P^+}(c_{\lambda,\mu,\nu}-d_\nu)\operatorname{ch}L(\nu)=0. \end{align*} Only finitely many coefficients in this sum are nonzero. By the [linear independence](/page/Linear%20Independence) proved in the previous step, \begin{align*} c_{\lambda,\mu,\nu}=d_\nu \end{align*} for every $\nu\in P^+$. Therefore the displayed character expansion uniquely determines the [irreducible decomposition](/theorems/2122) multiplicities $c_{\lambda,\mu,\nu}$ in $L(\lambda)\otimes L(\mu)$. [/step]