Tensor products of integrable highest weight modules decompose

Define $x(v\otimes w)=xv\otimes w+v\otimes xw$. This is balanced and linear in both tensor factors. Expanding the commutator of $x\otimes 1+1\otimes x$ and $y\otimes 1+1\otimes y$, the two mixed terms cancel because they act on different factors, leaving $[x,y]\otimes 1+1\otimes [x,y]$. Hence this is a Lie representation. For a fixed simple generator $x=e_i$ or $f_i$, choose $p,q\ge 1$ killing the fixed vectors $v,w$ under its powers, using F2. The two factor operators commute. In their $(p+q-1)$st binomial power, each term kills $v\otimes w$: its first exponent is at least $p$ or its second is at least $q$. A maximum over finitely many elementary tensors proves local nilpotence on every tensor vector.

The tensor weight decomposition is the algebraic direct sum of $V_{\eta }\otimes W_{\theta }$ grouped by $\eta +\theta$: every tensor is a finite sum of weight tensors, and the component maps induced by the factor projections prove directness before grouping. For $\nu =\lambda +\mu -\beta$, contributions have $\eta =\lambda -{\beta }_1$, $\theta =\mu -{\beta }_2$, with ${\beta }_1+{\beta }_2=\beta$ in $Q^{+}$. If $\beta =\sum b_i{\alpha }_i$, there are at most ${\prod }_i(b_i+1)$ such pairs, since each coefficient of ${\beta }_1$ lies between $0$ and $b_i$. By F3 and F5 each factor space is finite dimensional, so the finite sum of their tensor spaces is finite dimensional. Outside $(\lambda +\mu )-Q^{+}$ there are no contributions. Thus the tensor module belongs to $\mathcal{O}$ by F5.

Steps 1.1 and 1.2 give integrability and $\mathcal{O}$ membership. Apply F1 under the declared F4 assumption. Each copy of $L_A(\nu )$ in its direct sum has one nonzero top vector at weight $\nu$ by F3 and F5. In an internal direct sum these top lines are linearly independent. Their number is bounded by the finite dimension of the tensor weight space from 1.2: more than that many lines would supply a finite independent set larger than its dimension. Hence every simple has finite multiplicity. This is a finiteness assertion, not a closed tensor multiplicity formula.

At $\beta =0$ the only split is $(0,0)$, so the tensor top space is one dimensional. If a generator already kills either tensor factor, the bound in 1.1 remains valid with the corresponding exponent one. A zero factor would give the empty decomposition by the same argument, although the specified simple factors are nonzero. Zero dominant labels require no change. The nilpotence and weight-space calculations use only finite sums and finite bounds; AC is used precisely in invoking F1 for the decomposition.