Extraction of a Summand from a Finite Sum of Vectors

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

Let $b$ be a \reftext{def:finite-tuple-power-2026a}{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 \ref{lem:order-natural-numbers-2026a}; 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 \reftext{def:finite-sum-vector-space-2026a}{finite sums in $V$},