Finite sum of simple submodules
= Finite sum of simple submodules
{title2=$S_1+\cdots+S_n\text{ is semisimple}$}
A finite sum of <simple modules> inside one <module> is a <semisimple module>. Inductively, if $M$ is the sum already retained, then $M\cap S_j$ is a <submodule> of the <simple module> $S_j$, hence zero or $S_j$. In the first case append $S_j$ as a <direct summand>; in the second it adds nothing. This gives a <direct sum of modules> selected from the original family.