Proof of The Iterated Operation over a Finite Set Does Not Depend on the Enumeration

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Nonempty. By The Number of Elements of a Finite Set §cardinality, $n\in\mathbb{N}_{0}$ and there is a bijection $\varphi$ from $[n]$ onto $A$. If $n=0$, then $[n]=\emptyset$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, so $A=\varphi([n])=\emptyset$, contrary to the assumption. Hence $n\neq0$, and $n\in\mathbb{N}$ because $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets.

Independent. Let $\varphi$ and $\psi$ be bijections from $[n]$ onto $A$; here $n\in\mathbb{N}$ by the first part. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation, $\sigma=\varphi^{-1}\circ\psi$ is a bijection from $[n]$ onto $[n]$ with $\varphi(\sigma(k))=\psi(k)$ for all $k\in[n]$. Put $a_{k}=f(\varphi(k))$; then $a_{\sigma(k)}=f(\psi(k))$, and since $\ast$ is associative and commutative, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §reordering gives

$$\mathop{\ast}\limits_{k=1}^{n}f(\psi(k))=\mathop{\ast}\limits_{k=1}^{n}a_{\sigma(k)}=\mathop{\ast}\limits_{k=1}^{n}a_{k}=\mathop{\ast}\limits_{k=1}^{n}f(\varphi(k)).$$