Formally defining and understanding the summation over a finite set Let $S$ be a finite, nonempty set. Then there exists a positive integer $n$ and a bijective map $\phi: [n]\rightarrow S$, where $[n]:=[1, n]\cap \mathbb{Z}$. Let $(Y, +)$ be an abelian group, and $f: S\rightarrow Y$.
It seems that the summation over a set is defined to be
$$ \sum_{x\in S} f(x):=\sum_{i=1}^n  f(\phi(i)),$$
even though Wikipedia gives it as an identity (as if it would be a consequence of some more elementary properties; see the fourth identity in the Wikipedia page). It turns out that this is well-defined as the value does not depend on the choice of the bijection $\phi$.
So we have a rigorous definition for the sum. However, it is also important to have an intuitive understanding of it. We want $\Sigma_{x\in S} f(x)$ to mean that $f$ is evaluated at every element of $S$ precisely once, and those evaluations are added together; no other terms are added. What would be the easiest way to verify that the formal definition corresponds to intuition? Summations over a set are done all the time even without a thought, but I had never encountered the formal definition before. The definition seems to be somewhat complicated in the sense that it involves bijections, but we are dealing with something which you would expect to be very elementary.
 A: 
What would be the easiest way to verify that the formal definition corresponds to intuition?

This is an extremely difficult question to answer in general. I find an effective technique is coming up with a list of properties derived from intuition and verifying that our definition of $\sum$ is the only one that fits these properties.
For instance, based on your intuitive description, we should have the following properties:

*

*If $S = \{x\}$, then $\sum\limits_{s \in S} f(s) = f(x)$.

*Suppose we have $f : S \to Y$ and $g : R \to Y$ with $S, R$ disjoint and finite. Define $h(x) = \begin{cases} f(x) & x \in S \\ g(x) & x \in R \end{cases}$. Then $\sum\limits_{x \in S \cup R} h(x) = \sum\limits_{s \in S} f(s) + \sum\limits_{r \in R} g(r)$.

*$\sum\limits_{x \in \emptyset} f(x) = 0$
It turns out these three properties are enough to uniquely specify $\sum$. And the formal definition you provided meets our three criteria. This is as close as we can get to verifying that we’ve captured our intuition.
To prove this, consider any $\sum$ that satisfies the three above properties. Given any sequence $S_1, \ldots, S_n$ of pairwise disjoint sets and functions $f_i : S_i \to Y$ for each $i$, define $S = S_1 \cup \cdots \cup S_n$, and define $f : S \to Y$ by $f(x) = f_i(x)$ when $x \in S_i$. Then I claim $\sum\limits_{x \in S} f(x) = \sum\limits_{i = 1}^n \sum\limits_{x \in S_i} f_i(x)$. The proof is a straightforward induction using property 3 for the base case and property 2 for the inductive step.
Then given any bijection $\phi : [n] \to S$, define $S_i = \{\phi(i)\}$ and $f_i = f|_{S_i}$. Then using the above Lemma, we have $\sum\limits_{x \in S} f(x) = \sum\limits_{i = 1}^n \sum\limits_{x \in S_i} f_i(x)$. Using property 1, we have $\sum\limits_{x \in S_i} f_i(x) = f(\phi(i))$. So we do indeed have $\sum\limits_{x \in S} f(x) = \sum\limits_{i = 1}^n f(\phi(i))$.
