[proofplan] The forward direction extracts a vector from a non-trivial dependence relation: isolate a term with a non-zero coefficient and divide to express it as a linear combination of the remaining vectors. The reverse direction rearranges the expression $s_0 = \sum \lambda_i s_i$ into a non-trivial dependence relation by moving $s_0$ to the other side. [/proofplan] [step:Extract a vector from a non-trivial dependence relation ($\Rightarrow$)] Suppose $S$ is linearly dependent. Then there exist distinct elements $s_1, \ldots, s_n \in S$ and scalars $\mu_1, \ldots, \mu_n \in \mathbb{F}$, not all zero, such that \begin{align*} \sum_{i=1}^{n} \mu_i s_i = \mathbf{0}. \end{align*} Since not all $\mu_i$ are zero, there exists an index $j \in \{1, \ldots, n\}$ with $\mu_j \neq 0$. Relabel $s_0 := s_j$. Isolating the $j$-th term: \begin{align*} \mu_j s_0 = -\sum_{i \neq j} \mu_i s_i. \end{align*} Since $\mu_j \neq 0$ and $\mathbb{F}$ is a field, $\mu_j^{-1}$ exists. Multiplying both sides by $\mu_j^{-1}$: \begin{align*} s_0 = \sum_{i \neq j}\left(-\frac{\mu_i}{\mu_j}\right)s_i. \end{align*} Setting $\lambda_i = -\mu_i/\mu_j$ for $i \neq j$ and reindexing the remaining vectors as $s_1, \ldots, s_{n-1}$ gives the required expression. [guided] The definition of linear dependence gives a non-trivial relation $\sum \mu_i s_i = \mathbf{0}$ where "non-trivial" means at least one $\mu_j \neq 0$. The goal is to solve for $s_j$ in terms of the other vectors. Since $\mu_j \neq 0$ and we are working over a field (so every non-zero element has a multiplicative inverse), we can divide: \begin{align*} s_j = -\mu_j^{-1}\sum_{i \neq j}\mu_i s_i = \sum_{i \neq j}\left(-\frac{\mu_i}{\mu_j}\right)s_i. \end{align*} This expresses $s_j$ as a linear combination of the other elements of $S$. Note that the choice of $j$ is not unique --- any index with $\mu_j \neq 0$ works, and different choices may yield different vectors that can be expressed as combinations of the rest. [/guided] [/step] [step:Rearrange the linear combination into a dependence relation ($\Leftarrow$)] Suppose there exist distinct $s_0, s_1, \ldots, s_n \in S$ and scalars $\lambda_1, \ldots, \lambda_n \in \mathbb{F}$ with $s_0 = \sum_{i=1}^{n}\lambda_i s_i$. Rearranging: \begin{align*} (-1)s_0 + \sum_{i=1}^{n}\lambda_i s_i = \mathbf{0}. \end{align*} The coefficient of $s_0$ is $-1 \neq 0$, so this is a non-trivial linear relation among $n + 1$ distinct elements of $S$. By definition, $S$ is linearly dependent. [/step]