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.
Throughout, for a finite set C and a map u:C→X we use Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §empty as follows: if C=∅, then x∈C∗u(x)=e; if C=∅, then #C∈N by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and x∈C∗u(x)=k=1∗#Cu(γ(k)) for every bijection γ from [#C] onto C. If there is a bijection from [n] onto C with n∈N0, then n=#C by The Number of Elements of a Finite Set §cardinality. For u defined on a set containing C, the iterated operation over C is that of u∣C by Sums and Products over a Finite Set and over an Interval §subsets, and u∣C has the same values as u on C; we use this without comment. Finally e∗x=x∗e=x for every x∈X by Associative and Commutative Binary Operations, and Neutral Elements §neutral.
Singleton. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, [1]={1}, so γ:[1]→{y}, 1↦y, is a bijection and #{y}=1. By the first part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion, applied with n=1 to the map k↦f(γ(k)) on [1], k=1∗1f(γ(k))=f(γ(1)). Hence x∈{y}∗f(x)=f(γ(1))=f(y).
Disjoint union. If A=∅, then A∪B=B, and the right side is e∗x∈B∗f(x)=x∈B∗f(x), which is the left side; the case B=∅ is symmetric. Let A and B be nonempty, p=#A and q=#B, so p,q∈N, and let α and β be bijections from [p] onto A and from [q] onto B. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with m=1, n=p and q in place of p, whose hypothesis 1≤p+1 holds as 0≤p gives 1=0+1≤p+1 by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws, [p+q] is the union of the disjoint sets [p] and {p+1,…,p+q}, and by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift with m=1, n=q every element of the latter is p+j for exactly one j∈[q]; that is, j↦j+p=p+j is a bijection from [q] onto {p+1,…,p+q}, and we let θ be its inverse, a bijection from {p+1,…,p+q} onto [q] by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse. Define γ:[p+q]→A∪B by γ(k)=α(k) for k∈[p] and γ(k)=β(θ(k)) for the other k∈[p+q], a map by Maps Defined by Cases §cases with P(k) the property k∈[p]: for k∈[p], α(k)∈A, and for the other k, k∈{p+1,…,p+q} and β(θ(k))∈B. Thus γ(p+j)=β(j) for j∈[q]. Then γ maps [p] bijectively onto A and {p+1,…,p+q} bijectively onto B. Since A∩B=∅, two elements of [p+q] with the same image lie in the same one of these two pieces, so γ is injective; it is evidently surjective. Thus γ is a bijection from [p+q] onto A∪B, and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §splitting, applied to k↦f(γ(k)), gives
x∈A∪B∗f(x)=k=1∗p+qf(γ(k))=(k=1∗pf(α(k)))∗(j=1∗qf(β(j)))=(x∈A∗f(x))∗(x∈B∗f(x)).
Reindexing. If B=∅, then A=g(B)=∅, and both sides are e. Let B=∅, n=#B, and let β be a bijection from [n] onto B. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation, g∘β is a bijection from [n] onto A, so A=∅ and #A=n. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition,
y∈B∗f(g(y))=k=1∗nf(g(β(k)))=k=1∗nf((g∘β)(k))=x∈A∗f(x).
Product. First let A={a} be a singleton. The map y↦(a,y) from B to {a}×B and the map (a,y)↦y back are inverse to each other, so the former is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion. Reindexing along it and the singleton clause give
(x,y)∈{a}×B∗f(x,y)=y∈B∗f(a,y)=x∈{a}∗(y∈B∗f(x,y)).(1)
We prove the first equality of the clause. If A=∅, then A×B=∅ and both sides are e. We prove the first equality for nonempty A by induction from 1 on n=#A (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction), for all finite A with #A=n and all f; here n∈N. If #A=1, a bijection from [1]={1} onto A shows that A is a singleton, so the claim holds by (1). Suppose it holds for n, let #A=n+1, and let α be a bijection from [n+1] onto A. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, [n+1]=[n]∪{n+1} and n+1∈/[n]. Put A′=α([n]) and a=α(n+1). Then A=A′∪{a}, a∈/A′ as α is injective, and α∣[n] is a bijection from [n] onto A′, so #A′=n. Hence A×B is the union of the disjoint sets A′×B and {a}×B. The disjoint-union clause, the induction hypothesis for A′ and f∣A′×B, (1), and the disjoint-union clause for A=A′∪{a} and the map x↦y∈B∗f(x,y) give
(x,y)∈A×B∗f(x,y)=(x∈A′∗y∈B∗f(x,y))∗(x∈{a}∗y∈B∗f(x,y))=x∈A∗(y∈B∗f(x,y)).
So the claim holds for n+1. This proves the first equality for every finite A.
For the second equality, the map τ:B×A→A×B, (y,x)↦(x,y), is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion, the corresponding map A×B→B×A being its inverse. Reindexing along τ, and then the first equality with the roles of A and B exchanged, applied to f∘τ, give
(x,y)∈A×B∗f(x,y)=(y,x)∈B×A∗f(x,y)=y∈B∗(x∈A∗f(x,y)).
Termwise. If A=∅, both sides are e=e∗e. Otherwise, with n=#A and a bijection γ from [n] onto A, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §termwise applied to k↦f(γ(k)) and k↦g(γ(k)) gives
x∈A∗(f(x)∗g(x))=k=1∗n(f(γ(k))∗g(γ(k)))=(k=1∗nf(γ(k)))∗(k=1∗ng(γ(k)))=(x∈A∗f(x))∗(x∈A∗g(x)).
Homomorphism. If A=∅, the left side is φ(e)=e′, which is the right side. Otherwise, with n=#A and a bijection γ from [n] onto A, used for both ∗ and ⋄, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §homomorphism gives
φ(x∈A∗f(x))=φ(k=1∗nf(γ(k)))=k=1⋄nφ(f(γ(k)))=x∈A⋄φ(f(x)).
Interval recursion. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with p=1, whose hypothesis m≤n+1 is assumed, {m,…,n+1} is the union of the disjoint sets {m,…,n} and {n+1,…,n+1}={n+1}. By Sums and Products over a Finite Set and over an Interval §intervals and the disjoint-union and singleton clauses,
k=m∗n+1ak=(k∈{m,…,n}∗ak)∗(k∈{n+1}∗ak)=(k=m∗nak)∗an+1.
Interval shift. Let I={m,…,n} and J={m+p,…,n+p}, both finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, s:I→J, k↦k+p, is a bijection. In particular k+p∈J for every k∈I, so k↦ak+p is a map from I to X, and both sides of the clause are defined by Sums and Products over a Finite Set and over an Interval §intervals, since ∗ has the neutral element e; this covers the case m>n, in which I=∅ and J=s(I)=∅, so that both sides equal e. Let b=a∣J:J→X, so that b(s(k))=ak+p for k∈I. By Sums and Products over a Finite Set and over an Interval §intervals and the reindexing clause applied to the bijection s:I→J and the map b,
k=m∗nak+p=k∈I∗b(s(k))=j∈J∗b(j)=k=m+p∗n+pak.