Vector-space freeness from maximal independence (source code)

= Vector-space freeness from maximal independence
{title2=$V\cong\bigoplus_{b\in B}k$}

Order the <linearly independent> subsets of a <vector space> by inclusion. A chain's union is independent, since every finite relation is contained in one chain member. <Zorn's lemma> gives a maximal independent subset. A vector outside its span could be adjoined while preserving independence, so it spans. Sending finite-support coefficient families to their linear combinations gives an isomorphism from the <free module> on that subset to $V$. This supplies an arbitrary, possibly infinite-dimensional <basis> using the <axiom of choice>; no pre-existing <basis> theorem is invoked.