Summation over Finite Set is Well-Defined
Theorem
Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S$ be a finite set.
Let $f: S \to \mathbb A$ be a mapping.
Let $n$ be the cardinality of $S$.
let $\N_{<n}$ be an initial segment of the natural numbers.
Let $g, h: \N_{<n} \to S$ be bijections.
Then we have an equality of indexed summations of the compositions $f \circ g$ and $f \circ h$:
- $\ds \sum_{i \mathop = 0}^{n - 1} \map f {\map g i} = \sum_{i \mathop = 0}^{n - 1} \map f {\map h i}$
That is, the definition of summation over a finite set does not depend on the choice of the bijection $g: S \to \N_{< n}$.
Proof
By Inverse of Bijection is Bijection, $h^{-1} : \N_{<n} \to S$ is a bijection.
By Composite of Bijections is Bijection, the composition $h^{-1}\circ g$ is a permutation of $\N_{<n}$.
By Indexed Summation does not Change under Permutation, we have an equality of indexed summations:
- $\ds \sum_{i \mathop = 0}^{n - 1} \map {\paren {f \circ h} } i = \sum_{i \mathop = 0}^{n - 1} \map {\paren {f \circ h} \circ \paren {h^{-1} \circ g} } i$
By Composition of Mappings is Associative and Composite of Bijection with Inverse is Identity Mapping, the right hand side equals $\ds \sum_{i \mathop = 0}^{n - 1} \map f {\map g i}$.
$\blacksquare$