Extraction of a Summand from a Finite Sum of Vectors

Let $K$ be a field, let $V$ be a vector space over $K$, and let $n$ be a natural number. Inequalities between natural numbers use the order relations on $\mathbb{N}$.

Let $b$ be a tuple in $V^{n+1}$, with components $b_{k}$ for $1\le k\le n+1$, and let $j$ be a natural number with $j\le n+1$. Let $b^{(j)}$ be the tuple in $V^{n}$ with components

$$b^{(j)}_{k}=b_{k}\ \text{ for }k<j,\qquad b^{(j)}_{k}=b_{k+1}\ \text{ for }j\le k ,$$

where $k$ ranges over the natural numbers with $1\le k\le n$. Exactly one of the two cases applies to each such $k$, since the order on $\mathbb{N}$ is total by claim 3 of Properties of the Order on the Natural Numbers; and the components on the right are defined, since $k\le n+1$ and $k+1\le n+1$ by claims 1 and 6 of that lemma.

Then, with finite sums in $V$,

$$\sum_{k=1}^{n+1}b_{k}=\Bigl(\sum_{k=1}^{n}b^{(j)}_{k}\Bigr)+b_{j}.$$