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

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$,