Choice-free semisimple characterizations for finite-length modules

Suppose $M$ is a sum of simple submodules and start with $D_0=0$. If $D_k\mathrm{\ne }M$, some simple $S_k$ is not contained in $D_k$, so simplicity gives $S_k\cap D_k=0$ and $D_{k+1}=D_k\oplus S_k$. Intersecting a fixed $n$-factor composition series of $M$ with $D_k$ and deleting repetitions gives a composition series of $D_k$ with at most $n$ factors. Since $D_k$ already has the $k$-factor series obtained by adding the $S_j$ one at a time, [L2] gives $k\le n$. Thus after at most $n$ finite choices the process reaches $M$, proving that a sum of simples is a finite direct sum without any choice axiom.

Now write a finite direct-sum decomposition $M={⨁}_{i=1}^t{S}_i$ and let $N\le M$. Process the finitely many $S_i$ in order, maintaining a sum $C$ with $C\cap N=0$: add $S_i$ exactly when $S_i\le ̸N+C$. In that case simplicity gives $S_i\cap (N+C)=0$, so the invariant persists. At the end every $S_i\le N+C$, whence $M=N\oplus C$. This proves that the direct-sum condition implies the complement condition without Zorn.

Conversely, suppose every submodule of the finite-length module $M$ has a complement, and induct on a fixed composition-series length. If $M\mathrm{\ne }0$, let $A$ be the penultimate term of such a series. A complement $S$ gives $M=A\oplus S$ with $S\cong M\mathrm{/}A$ simple. The complement property passes to $A$: for $L\le A$, if $M=L\oplus D$, then $A=L\oplus (A\cap D)$. The induction hypothesis makes $A$ a finite direct sum of simples, hence so is $M$. Together with step 1.1 and the trivial direct-sum-to-sum implication, this proves all three equivalences, including lengths zero and one, without Choice.