Basis partition gives a module direct sum (source code)

= Basis partition gives a module direct sum
{title2=$E=E'\sqcup E''\Longrightarrow M=\langle E'\rangle\oplus\langle E''\rangle$}

Partition a <basis of a module> $E$ into disjoint subsets $E',E''$. Splitting the finite expression of each element gives $M=\langle E'\rangle+\langle E''\rangle$. An element in both generated <submodules> would give, by subtraction, a relation among the disjoint parts of $E$; <linear independence in a module> forces every coefficient to vanish. The intersection is zero, proving the <direct sum of modules> decomposition. Each part is itself a <basis of a module> for the <submodule> it generates.