Linearly_Dependent_Sequence_of_Vector_Space

Let $\struct {G, +}$ be a group whose identity is $\mathbf 0$. Let $\struct {G, +, \circ}_K$ be a $K$-vector space. Let $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ be a sequence of distinct non-zero vectors of $G$. Then $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ is linearly dependent $\exists p \in \closedint 2 n: a_p$ is a linear combination of $\sequence {a_k}_{1 \mathop \le k \mathop \le p - 1}$