Proof of A Sum over a Finite Index Set Does Not Depend on the Enumeration

By Bijection of Sets the bijection $\varphi$ has an inverse map $\varphi^{-1}:F\to[n]$, which is itself a bijection, and $\varphi^{-1}(\varphi(k))=k$ for every $k\in[n]$ while $\varphi(\varphi^{-1}(x))=x$ for every $x\in F$. By claim 2 of Injectivity, Composition, and Restriction of Bijections the map $\sigma:[n]\to[n]$ given by $\sigma(k)=\varphi^{-1}\bigl(\psi(k)\bigr)$ is a bijection.

Let $a:[n]\to K$ be the map with $a_{k}=f\bigl(\varphi(k)\bigr)$. For every $k\in[n]$,

Hence claim 1 of Invariance of Finite Sums and Products under Reindexing by a Permutation, applied to $a$ and $\sigma$, gives