Properties of a Sum over a Finite Index Set

Let $K$ be a field, let $F$ and $G$ be nonempty finite sets, let $f:F\to K$ and $h:F\to K$ be maps, and let $\lambda\in K$. Sums over a finite index set are those of Sum over a Finite Index Set, and sums with a numerical index range are the finite sums of $K$.

Then the following hold.

1. (Agreement with an indexed sum) Let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$, and let $c:[n]\to K$ be a map with values $c_{k}$. Then $[n]$ is a nonempty finite set and

2. (Reindexing along a bijection) Let $\theta:G\to F$ be a bijection. Then

3. (Additivity) Writing $f+h$ for the map whose value at $x$ is $f(x)+h(x)$,

4. (Homogeneity)