Solution (source code)

= Solution

We first prove that every extension of two simple modules splits. Consider
$$
0\longrightarrow A_n\longrightarrow V\longrightarrow A_m\longrightarrow0.
$$
If $n\ne m$, the central <Casimir element> has distinct scalars $n(n+2)$ and $m(m+2)$. On $V$ its <minimal polynomial> divides the product of the corresponding two distinct linear factors. Its eigenspaces are submodules, and the <eigenspace> for $m(m+2)$ maps isomorphically onto the <quotient>. It is the required complement.

Now suppose $n=m=l$. Use <generalized weight spaces> for $H$; their possible weights are $l,l-2,\ldots,-l$, because the <characteristic polynomial> on an extension is the product of those on its two factors. Lift the <quotient>'s highest vector to $w$ in the <generalized weight space> of <representation weight> $l$. Then $ew=0$ and $f^{l+1}w=0$, since these would lie in <generalized weight spaces> of weights $l+2$ and $-l-2$, which are absent. Also $(H-l)w=av_0$ for a highest vector $v_0$ in the <submodule> $A_l$. The commutator identity gives
$$
0=ef^{l+1}w=(l+1)f^l(H-l)w=(l+1)a f^lv_0.
$$
Thus $a=0$. The vector $w$ is an actual highest-<weight vector>. Its lowering chain maps to the full <basis> of the <quotient>, so it generates an $A_l$ complementary to the original <submodule>. This proves splitting also when the two simple types coincide, including $l=0$.

The same splitting holds for a semisimple <kernel> and simple <quotient> by induction on the number of <kernel> summands. Write the <kernel> as $U_1\oplus U_2$ with $U_1$ simple. Modulo $U_2$, split the extension by the simple <quotient>; the inverse image of that chosen <quotient> copy is an extension with <kernel> $U_2$. Split it inductively, obtaining a <submodule> in $V$ meeting the entire original <kernel> trivially.

Finally induct on $\dim V$. A maximal proper <submodule> has smaller <dimension> and hence is semisimple by induction; the <quotient> is simple by maximality. The just-proved splitting completes the induction. Hence
$$
\boxed{V\cong\bigoplus_{l\ge0}A_l^{\oplus m_l},\qquad m_l\in\mathbb Z_{\ge0},}
$$
with only finitely many nonzero multiplicities. This proof does not assume the complete-reducibility theorem it is establishing.