Proof of Properties of a Sum over a Finite Index Set

Throughout, for a nonempty finite set $E$ we write $|E|$ for the natural number such that $E$ has that many elements, unique by Uniqueness of the Number of Elements, and we evaluate $\sum_{x\in E}$ using Sum over a Finite Index Set with a bijection $[\,|E|\,]\to E$ of our choosing, which is legitimate by A Sum over a Finite Index Set Does Not Depend on the Enumeration.

Claim 1. The identity map of $[n]$ is a bijection from $[n]$ onto $[n]$, so $[n]$ has $n$ elements in the sense of Number of Elements of a Set, and $[n]$ is a nonempty finite set since $1\in[n]$. Evaluating $\sum_{x\in[n]}c(x)$ with the identity map as the bijection $\varphi$ gives $\sum_{x\in[n]}c(x)=\sum_{k=1}^{n}c(k)=\sum_{k=1}^{n}c_{k}$.

Claim 2. Let $n=|F|$ and let $\varphi:[n]\to F$ be a bijection. By Bijection of Sets the bijection $\theta$ has an inverse $\theta^{-1}:F\to G$, which is a bijection, so by claim 2 of Injectivity, Composition, and Restriction of Bijections the map $\chi:[n]\to G$ given by $\chi(k)=\theta^{-1}\bigl(\varphi(k)\bigr)$ is a bijection. In particular $G$ has $n$ elements, so $|G|=n$ by Uniqueness of the Number of Elements. Evaluating the left-hand side with $\chi$ and the right-hand side with $\varphi$, and using $\theta\bigl(\theta^{-1}(x)\bigr)=x$,

$$\sum_{y\in G}f\bigl(\theta(y)\bigr)=\sum_{k=1}^{n}f\Bigl(\theta\bigl(\theta^{-1}(\varphi(k))\bigr)\Bigr)=\sum_{k=1}^{n}f\bigl(\varphi(k)\bigr)=\sum_{x\in F}f(x).$$

Claims 3 and 4. Let $n=|F|$ and let $\varphi:[n]\to F$ be a bijection; evaluate all three sums in claim 3, and both sums in claim 4, using this same $\varphi$. Claim 3 is then claim 2 of Properties of Finite Sums applied to the maps $k\mapsto f(\varphi(k))$ and $k\mapsto h(\varphi(k))$, and claim 4 is claim 3 of that lemma applied to the map $k\mapsto f(\varphi(k))$ with the scalar $\lambda$.