Sum over a Finite Index Set

Let $K$ be a field, let $F$ be a nonempty finite set, let $n$ be the natural number for which $F$ has $n$ elements, unique by Uniqueness of the Number of Elements, let $[n]$ be the initial segment determined by $n$, and let $f:F\to K$ be a map.

The sum of $f$ over $F$ is

where $\varphi:[n]\to F$ is any bijection and the right-hand side is the finite sum of $K$. At least one such $\varphi$ exists because $F$ has $n$ elements, and the right-hand side does not depend on the choice of $\varphi$ by A Sum over a Finite Index Set Does Not Depend on the Enumeration.