Span equals finite linear combinations

Theorem. Let $X$ be a vector space over $K$, and let $A\subseteq X$. Then the span of $A$ is

the set of all finite linear combinations of elements of $A$. The case $m=0$ denotes the empty sum $0$, so the formula also covers $A=\varnothing$.

Proof sketch. Let $Y$ be the set of all such finite linear combinations. One checks that $Y$ is a linear subspace and contains $A$, hence $\operatorname{span}(A)\subset Y$ by minimality. Conversely, $\operatorname{span}(A)$ is a subspace containing $A$, so it is closed under forming finite linear combinations of elements of $A$, giving $Y\subset \operatorname{span}(A)$.