avewright/proofwiki-math huggingface dataset:
Theorem: Infinite Set is Equivalent to Proper Subset

A set is infinite {{iff}} it is equivalent to one of its proper subsets.

Proof:
Let $T$ be an infinite set.
By Infinite Set has Countably Infinite Subset, it is possible to construct a countably infinite subset of $T$.
Let $S = \set {a_1, a_2, a_3, \ldots}$ be such a countably infinite subset of $T$.
Create a Partition of $S$ into:
:$S_1 = \set {a_1, a_3, a_5, \ldots}, S_2 = \set {a_2, a_4, a_6, \ldots}$
Let a bijection be established between $S$ and $S_1$, by letting $a_n \leftrightarrow a_{2 n - 1}$.
This is extended to a bijection between $S \cup \paren {T \setminus S} = T$ and $S_1 \cup \paren {T \setminus S} = T \setminus S_2$ by assigning each element in $T \setminus S$ to itself.
So a bijection has been demonstrated between $T$ and one of its proper subsets $T \setminus S_2$.
That is, if $T$ is infinite, it is equivalent to one of its proper subsets.
Now, let $T_0 \subsetneq T$ be a proper subset of $T$, and $f: T \to T_0$ be a bijection.
It follows from No Bijection between Finite Set and Proper Subset that $T$ must be infinite.
{{qed}}
Theorem: Infinite Set is Equivalent to Proper Subset

A set is infinite {{iff}} it is equivalent to one of its proper subsets.

Proof:
Let $S$ be a set.
Suppose $S$ is finite.
From No Bijection between Finite Set and Proper Subset we have that $S$ can not be equivalent to one of its proper subsets.
Suppose $S$ is infinite.
From Infinite Set has Countably Infinite Subset, we can construct $v: \N \to S$ such that $v$ is an injection.
We now construct the mapping $h: S \to S$ as follows.
:$\map h x = \begin {cases}
\map v {n + 1} & : \exists n \in \N: x = \map v n \\
x & : x \notin \Img v
\end {cases}$
It is clear that $h$ is an injection.
But we have that $\map v 0 \notin \Img h$ and so $\Img h \subsetneq S$.
The result follows from Injection to Image is Bijection.
{{qed}}
Theorem: Infinite Set is Equivalent to Proper Subset

A set is infinite {{iff}} it is equivalent to one of its proper subsets.

Proof:
Let $X$ be a set which has a proper subset $Y$ such that:
:$\card X = \card Y$
where $\card X$ denotes the cardinality of $X$.
Then:
:$\exists \alpha \in \complement_X \paren Y$
and
:$Y \subsetneqq Y \cup \set \alpha \subseteq X$
The inclusion mappings:
:$i_Y: Y \to X: \forall y \in Y: i \paren y = y$
:$i_{Y \cup \set \alpha}: Y \cup \set \alpha \to X: \forall y \in Y: i \paren y = y$
give:
:$\card X = \card Y \le \card Y + \mathbf 1 \le \card X $
from which:
:$\card X = \card Y + \mathbf 1 = \card X + \mathbf 1$
So by definition $X$ is infinite.
{{qed|lemma}}
Now suppose $X$ is infinite.
That is:
:$\card X = \card X + \mathbf 1$
Let $\alpha$ be any object such that $\alpha \notin X$.
Then there is a bijection $f: X \cup \set \alpha \to X$.
Let $f_{\restriction X}$ be the restriction of $f$ to $X$.
Then from Injection to Image is Bijection:
:$\image {f_{\restriction X} } = X \setminus \set {f \paren \alpha}$
which is a proper subset of $X$ which is equivalent to $X$.
{{qed}}
Theorem: Cartesian Product of Countable Sets is Countable

The cartesian product of two countable sets is countable.

Proof:
Let $S_1, S_2, \ldots, S_k$ be countable sets. Equivalently, there exists an injection $f_i: S_i \to \N$ for each $i \in \{ 1, \dots, k \}$.
Therefore, the mapping $g: S_1 \times S_2 \times \cdots \times S_k \to \N^k$ defined by (for $x_i \in S_i$):
:$\map g {x_1, x_2, \dotsc, x_k} = \tuple {\map {f_1} {x_1}, \map {f_2} {x_2}, \dotsc, \map {f_k} {x_k} }$
is also injective.
Now let $p_1, p_2, \ldots, p_k$ be the first $k$ prime numbers.
From the Fundamental Theorem of Arithmetic, $f: \N^k \to \N$ defined as:
:$\map f {n_1, n_2, \ldots, n_k} = p_1^{n_1} p_2^{n_2} \cdots p_k^{n_k}$
is an injection.
From Composite of Injections is Injection, $f \circ g: S_1 \times S_2 \times \cdots \times S_k \to \N$ is injective.
{{qed}}
Theorem: Cartesian Product of Countable Sets is Countable

The cartesian product of two countable sets is countable.

Proof:
Proof by induction:
=== Basis for the Induction ===
When $k = 2$, the case is the same as Cartesian Product of Countable Sets is Countable.
So shown for basis for the induction.
=== Induction Hypothesis ===
This is our induction hypothesis:
:$\exists f_k: S_1 \times S_2 \times \cdots \times S_k \to \N$
where $f_k$ is an injection.
Now we need to show that for $n = k + 1$:
:$\exists f_{k+1}: S_1 \times S_2 \times \cdots \times S_k \times S_{k+1} \to \N$
where $f_{k+1}$ is an injection.
=== Induction Step ===
This is our induction step:
By the induction hypothesis:
:$\exists f_k: S_1 \times S_2 \times \cdots \times S_k \to \N$
where $f_k$ is an injection.
Thus by definition, $S_1 \times S_2 \times \cdots \times S_k$ is countable.
By hypothesis $S_{k + 1}$ is countable.
So by the basis for the induction:
:$\exists g: \left({S_1 \times S_2 \times \cdots \times S_k}\right) \times S_{k+1} \to \N \times \N$
where $g$ is an injection.
By Cartesian Product of Countable Sets is Countable,
:$\exists r: \N \times \N \to \N$
where $r$ is an injection.
Therefore, by Composite of Injections is Injection:
:$f_{k+1} = r \circ g: S_1 \times S_2 \times \cdots \times S_k \times S_{k+1} \to \N$
is an injection.
The result follows by induction.
{{qed}}
Theorem: Cartesian Product of Countable Sets is Countable

The cartesian product of two countable sets is countable.

Proof:
Let $S, T$ be countable sets.
From the definition of countable, there exists a injection from $S$ to $\N$, and similarly one from $T$ to $\N$.
Hence there exists an injection $g$ from $S \times T$ to $\N^2$.
Now let us investigate the cardinality of $\N^2$.
From the Fundamental Theorem of Arithmetic, every natural number greater than $1$ has a unique prime decomposition.
Thus, if a number can be written as $2^n 3^m$, it can be done thus in only one way.
So, consider the function $f: \N^2 \to \N$ defined by:
:$\map f {n, m} = 2^n 3^m$.
Now suppose $\exists m, n, r, s \in \N$ such that $\map f {n, m} = \map f {r, s}$.
Then $2^n 3^m = 2^r 3^s$ so that $n = r$ and $m = s$.
Thus $f$ is an injection, whence $\N^2$ is countably infinite.
Now we see that as $g$ and $f$ are injective, it follows from Composite of Injections is Injection that $f \circ g: S \times T \to \N$ is also injective.
Hence the result.
{{qed}}
Theorem: Cartesian Product of Countable Sets is Countable

The cartesian product of two countable sets is countable.

Proof:
Let $S = \set {s_0, s_1, s_2, \dotsc}$ and $T = \set {t_0, t_1, t_2, \dotsc}$ be countable sets.
If both $S$ and $T$ are finite, the result follows immediately.
Suppose either of $S$ or $T$ (or both) is countably infinite.
We can write the elements of $S \times T$ in the form of an infinite table:
$\quad \begin{array} {*{4}c}
\tuple {s_0, t_0} & \tuple {s_0, t_1} & \tuple {s_0, t_2} & \cdots \\
\tuple {s_1, t_0} & \tuple {s_1, t_1} & \tuple {s_1, t_2} & \cdots \\
\tuple {s_2, t_0} & \tuple {s_2, t_1} & \tuple {s_2, t_2} & \cdots \\
\vdots  & \vdots  & \vdots & \ddots \\
\end{array}
$
This table clearly contains all the elements of $S \times T$.
Now we can count the elements of $S \times T$ by processing the table diagonally.
First we pick $\tuple {s_0, t_0}$.
Then we pick $\tuple {s_0, t_1}, \tuple {s_1, t_0}$. Then we pick $\tuple {s_0, t_2}, \tuple {s_1, t_1}, \tuple {s_2, t_0}$.
We can see that all the elements of $S \times T$ will (eventually) be listed, and there is a specific number (element of $\N$) to index each of its elements with.
Thus we have the required one-to-one correspondence between $S \times T$ and $\N$, and our assertion is proved.
{{qed}}
Theorem: Composition of Sequence with Mapping

Let $\sequence {a_j}_{j \mathop \in B}$ be a sequence.
Let $\sigma: A \to B$ be a mapping, where $A \subseteq \N$.
Then $\sequence {a_j} \circ \sigma$ is a sequence whose value at each $k \in A$ is $a_{\map \sigma k}$.
Thus $\sequence {a_j} \circ \sigma$ is denoted $\sequence {a_{\map \sigma k} }_{k \mathop \in A}$.

Proof:
By definition, a sequence is a mapping whose domain is a subset of $\N$.
Let the range of $\sequence {a_j}_{j \mathop \in B}$ be $S$.
Thus $\sequence {a_j}_{j \mathop \in B}$ can be expressed using the mapping $f: B \to S$ as:
:$\forall j \in B: \map f j = a_j$
Let $k \in A$.
Then $\map \sigma k \in B$.
By definition of composition of mappings:
{{begin-eqn}}
{{eqn | l = f \circ \map \sigma k
      | r = \map f {\map \sigma k}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sequence {a_j}_{j \mathop \in B}
      | r = \sequence {a_{\map \sigma k} }_{\map \sigma k \mathop \in B}
      | c = 
}}
{{eqn | r = \sequence {a_{\map \sigma k} }_{k \mathop \in A}
      | c = as $\map \sigma k \in B \implies k \in A$
}}
{{end-eqn}}
{{qed}}
Category:Sequences
37t0jwve7ojqa8z70f1i5su7bjf4c0h
Theorem: General Operation from Binary Operation

Let $\struct {S, \oplus}$ be a magma.
Then there a unique sequence $\sequence {\oplus_k}_{k \mathop \ge 1}$ such that:
:$(1): \quad \forall n \in \N_{>0}: \oplus_n$ is an $n$-ary operation on $S$ such that:
:$(2): \quad \forall \tuple {a_1, \ldots, a_k} \in S^k: \map {\oplus_k} {a_1, \ldots, a_k} = \begin{cases}
a : & k = 1 \\
\map {\oplus_n} {a_1, \ldots, a_n} \oplus a_{n + 1} : & k = n + 1
\end{cases}$
In particular, $\oplus_2$ is the same as the given binary operation $\oplus$.
The $n$th term $\oplus_n$ of the sequence $\sequence \oplus$ is called the '''$n$-ary operation defined by $\oplus$'''.

Proof:
Let $\Bbb S = \leftset {\odot:}$ for some $n \in \N_{>0}$, $\odot$ is an $n$-ary operation on $\rightset S$.
Let $s: \Bbb S \to \Bbb S$ be the mapping defined as follows.
Let $\odot$ be any $n$-ary operation defined on $\Bbb S$.
Then $\map s \odot$ is the $\paren {n + 1}$-ary operation defined by:
:$\forall \tuple {a_1, \ldots, a_n, a_{n + 1} } \in S^{n + 1}: \map {\map s \odot} {a_1, \ldots, a_n, a_{n + 1} } = \map \odot {a_1, \ldots, a_n} \oplus a_{n + 1}$
By the Principle of Recursive Definition, there is a unique sequence $\sequence {\oplus_k}_{k \mathop \ge 1}$ such that:
:$\oplus_1$ is the unary operation defined as $\map {\oplus_1} a = a$
and:
:$\oplus_{n + 1} = \map s {\oplus_n}$ for each $n \in \N_{>0}$.
Let $A$ be the set defined as the set of all $n$ such that:
:$\oplus_n$ is an $n$-ary operation on $S$
and:
:by the definition of $s$, $(2)$ holds for every ordered $n + 1$-tuple in $S^{n + 1}$.
It will be demonstrated by the Principle of Mathematical Induction that $A = \N$.
Theorem: Strictly Increasing Sequence induces Partition

Let $\sequence {r_k}_{0 \mathop \le k \mathop \le n}$ be a strictly increasing finite sequence of natural numbers.
Let:
:$\forall k \in \closedint 1 n: A_k := \closedint {r_{k - 1} + 1} {r_k}$
Then:
:$\set {A_k: k \in \closedint 1 n}$ is a partition of $\closedint {r_0 + 1} {r_n}$.

Proof:
First we show that the elements of $\set {A_k: k \in \closedint 1 n}$ are disjoint.
Let $j \in \closedint 1 n$.
We have that:
:$\sequence {r_k}_{0 \mathop \le k \mathop \le n}$ is strictly increasing
and:
:$0 \le j - 1 < j \le n$
Thus by Sum with One is Immediate Successor in Naturally Ordered Semigroup:
:$r_0 \le r_{j - 1} < r_j \le r_n \implies \paren {r_0 + 1} \le \paren {r_{j - 1} + 1} \le r_j \le r_n$
So:
:$\O \subset A_j \subseteq \closedint {r_0 + 1} {r_n}$
Because $\sequence {r_k}_{0 \mathop \le k \mathop \le n}$ is strictly increasing:
:$1 \le j < k \le n \implies A_j \cap A_k = \O$
So the elements of $\set {A_k: k \in \closedint 1 n}$ are disjoint, as we were to show.
It remains to be established that:
:if $m \in \closedint {r_0 + 1} {r_n}$
then:
:$m \in A_k$ for some $k \in \closedint 1 n$.
Let $m \in \closedint {r_0 + 1} {r_n}$.
Consider the set:
:$J = \set {j \in \closedint 0 n: m \le r_j}$
Clearly $j \ne \O$ as $n \in J$.
Let $k$ be the smallest element of $J$.
Then because $r_0 < m$:
:$k \ne 0$
Thus:
:$k \in \closedint 1 n$
By its definition:
:$r_{k - 1} < m \le r_k$
Thus, by Sum with One is Immediate Successor in Naturally Ordered Semigroup:
:$r_{k - 1} + 1 \le m \le r_k$
Therefore $m \in A_k$.
{{qed}}
{{improve|A better link instead of Sum with One is Immediate Successor in Naturally Ordered Semigroup}}
Theorem: Fundamental Principle of Counting

Let $A$ be a finite set.
Let $\sequence {B_n}$ be a sequence of distinct finite subsets of $A$ which form a partition of $A$.
Let $p_k = \size {B_k}$ for each $k \in \closedint 1 n$.
Then:
:$\ds \size A = \sum_{k \mathop = 1}^n p_k$
That is, the sum of the numbers of elements in the subsets of a partition of a set is equal to the total number of elements in the set.

Proof:
Let $r_0 = 0$, and let:
:$\ds \forall k \in \closedint 1 n: r_k = \sum_{j \mathop = 1}^k {p_j}$
Then:
:$r_{k - 1} + p_k = r_k$
so:
:$r_{k - 1} < r_k$.
Thus by Isomorphism to Closed Interval, $\closedint {r_{k - 1} } {r_k}$ has $r_k - r_{k - 1} = p_k$ elements.
As a consequence, there exists a bijection $\sigma_k: B_k \to \closedint {r_{k - 1} } {r_k}$ for each $k \in \closedint 1 n$.
Let $\sigma: A \to \N$ be the mapping that satisfies:
:$\forall x \in B_k: \forall k \in \N: \map \sigma x = \map {\sigma_k} x$
By Strictly Increasing Sequence on Ordered Set, $\sequence {r_k}_{0 \mathop \le k \mathop \le n}$ is a strictly increasing sequence of natural numbers.
Thus by Strictly Increasing Sequence induces Partition, $\sigma: A \to \closedint 1 {r_n}$ is a bijection.
By Isomorphism to Closed Interval, $\closedint 1 {r_n}$ has $r_n$ elements.
Hence the result.
{{Qed}}
Theorem: Odd Number Theorem

:$\ds \sum_{j \mathop = 1}^n \paren {2 j - 1} = n^2$
That is, the sum of the first $n$ odd numbers is the $n$th square number.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 1}^n \paren {2 j - 1}
      | r = n^2
      | c = Odd Number Theorem
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 1}^n \paren {2 j - 1} + \sum_{j \mathop = 1}^n 1
      | r = n^2 + n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 1}^n \paren {2 j}
      | r = n \paren {n + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 1}^n j
      | r = \frac {n \paren {n + 1} } 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Odd Number Theorem

:$\ds \sum_{j \mathop = 1}^n \paren {2 j - 1} = n^2$
That is, the sum of the first $n$ odd numbers is the $n$th square number.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 1}^n \paren {2 j - 1}
      | r = 2 \sum_{j \mathop = 1}^n j - \sum_{j \mathop = 1}^n 1
      | c = Linear Combination of Indexed Summations
}}
{{eqn | r = 2 \paren {\frac {n \paren {n + 1} } 2} - n
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = n^2 + n - n
}}
{{eqn | r = n^2
}}
{{end-eqn}}
{{qed}}
Theorem: General Associativity Theorem

If an operation is associative on $3$ entities, then it is associative on any number of them.

Proof:
The cases where $n = 1$ and $n = 2$ are clear.
Let $a = x \circ y \in P_n: x \in P_r, y \in P_s$.
If $r > 1$ then we write $x = a_1 \circ z$ where $z = a_2 \circ a_3 \circ \ldots \circ a_r$ by induction.
Then $x \circ y = \paren {a_1 \circ z} \circ y = a_1 \circ \paren {z \circ y} = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$ (again by induction).
If $r = 1$, then by induction $x \circ y = a_1 \circ y = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$.
Thus in either case, $x \circ y = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$ which is a single element of $P_n$.
Hence we see that $\map {P_n} {a_1, a_2, \ldots, a_n}$ consists of a single element.
{{Qed}}
Theorem: General Associativity Theorem

If an operation is associative on $3$ entities, then it is associative on any number of them.

Proof:
Proof by strong induction:
For all $n \in \N_{> 0}$, let $P \left({n}\right)$ be the proposition:
:The General Associativity Theorem holds for all composites $a_1 \circ a_2 \circ \cdots \circ a_r$ such that $r \le n$.
$P \left({1}\right)$ is trivially true, as this just says $a_1 = a_1$.
$P \left({2}\right)$ is the case:
:$a_1 \circ a_2 = a_1 \circ a_2$
for which there is also nothing to prove.
=== Basis for the Induction ===
$P \left({3}\right)$ is the case:
:$\left({a_1 \circ a_2}\right) \circ a_3 = a_1 \circ \left({a_2 \circ a_3}\right)$
which is the definition of associativity.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $P \left({k}\right)$ is true, where $k \ge 3$, then it logically follows that $P \left({k+1}\right)$ is true.
So this is our induction hypothesis:
:The General Associativity Theorem holds for all composites $a_1 \circ a_2 \circ \cdots \circ a_r$ such that $r \le k$.
Then we need to show:
:The General Associativity Theorem holds for all composites $a_1 \circ a_2 \circ \cdots \circ a_r$ such that $r \le k+1$.
=== Induction Step ===
This is our induction step:
Consider the expressions:
:$(1): \quad \left({a_1 \circ a_2 \circ \cdots \circ a_i}\right) \circ \left({a_{i+1} \circ a_{i+2} \circ \cdots \circ a_{k+1}}\right)$
:$(2): \quad \left({a_1 \circ a_2 \circ \cdots \circ a_j}\right) \circ \left({a_{j+1} \circ a_{i+2} \circ \cdots \circ a_{k+1}}\right)$
for some $i, j \in \Z: 1 \le i, j \le k$.
We require to show that whatever the values of $i$ and $j$, these expressions are equal.
{{WLOG}}, suppose that $i < j$.
Then the above expressions can be written:
:$\left({a_1 \circ a_2 \circ \cdots \circ a_i}\right) \circ \left({a_{i+1} \circ a_{i+2} \circ \cdots \circ a_j}\right) \circ \left({a_{j+1} \circ a_{i+2} \circ \cdots \circ a_{k+1}}\right)$
By the basis for the induction, the General Associativity Theorem holds for each of the parts in parenthesis.
Let:
: $a = \left({a_1 \circ a_2 \circ \cdots \circ a_i}\right)$
: $b = \left({a_{i+1} \circ a_{i+2} \circ \cdots \circ a_j}\right)$
: $c = \left({a_{j+1} \circ a_{i+2} \circ \cdots \circ a_{k+1}}\right)$
By definition of associative operation:
:$\left({a \circ b}\right) \circ c = a \circ \left({b \circ c}\right)$
This demonstrates the equality of the expressions $(1)$ and $(2)$.
So $P \left({k}\right) \implies P \left({k+1}\right)$ and the result follows by the Second Principle of Mathematical Induction.
Therefore:
:The General Associativity Theorem holds for all composites $a_1 \circ a_2 \circ \cdots \circ a_n$ for $n \in \N$.
{{qed}}
Theorem: General Commutativity Theorem

Let $\struct {S, \circ}$ be a semigroup.
Let $\family {a_k}_{1 \mathop \le k \mathop \le n}$ be a sequence of elements of $S$.
Suppose that:
:$\forall i, j \in \closedint 1 n: a_i \circ a_j = a_j \circ a_i$
Then for every permutation $\sigma: \N_n \to \N_n$:
:$a_{\map \sigma 1} \circ \cdots \circ a_{\map \sigma n} = a_1 \circ \cdots \circ a_n$
where $\N_n$ is used here to denote the initial segment of $\N_{>0}$:
:$\N_n = \set {1, 2, \ldots, n}$

Proof:
The proof will proceed by the Principle of Mathematical Induction on $\N_{>0}$.
Let $T$ be the set of all $n \in \N_{>0}$ such that:
:$a_{\map \sigma 1} \circ \cdots \circ a_{\map \sigma n} = a_1 \circ \cdots \circ a_n$
holds for all sequences $\sequence {a_k}_{1 \mathop \le k \mathop \le n}$ of $n$ elements of $S$ which satisfy:
:$\forall i, j \in \closedint 1 n: a_i \circ a_j = a_j \circ a_i$
for every permutation $\sigma: \N_n \to \N_n$.
Theorem: General Distributivity Theorem

:$\ds \paren {\sum_{i \mathop = 1}^m a_i} * \paren {\sum_{j \mathop = 1}^n b_j} = \sum_{\substack {1 \mathop \le i \mathop \le m \\ 1 \mathop \le j \mathop \le n} } \paren {a_i * b_j}$

Proof:
Proof by induction:
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\ds \forall m \in \Z_{> 0}: \paren {\sum_{i \mathop = 1}^m a_i} * \paren {\sum_{j \mathop = 1}^n b_j} = \sum_{\substack {1 \mathop \le i \mathop \le m \\ 1 \mathop \le j \mathop \le n} } \paren {a_i * b_j}$
We have that $\struct {R, \circ, *}$ is a ringoid, and so:
:$\forall a, b, c \in S: \paren {a \circ b} * c = \paren {a * c} \circ \paren {b * c}$
:$\forall a, b, c \in R: a * \paren {b \circ c} = \paren {a * b} \circ \paren {a * c}$
Theorem: Associativity on Indexing Set

Let $\struct {S, \circ}$ be a commutative semigroup.
Let $\family {x_\alpha}_{\alpha \mathop \in A}$ be a family of terms of $S$ indexed by a finite non-empty set $A$.
Let $\family {B_k}_{1 \mathop \le k \mathop \le n}$ be a family of distinct subsets of $A$ forming a partition of $A$.
Then:
:$\ds \prod_{k \mathop = 1}^n \paren {\prod_{a \mathop \in B_k} x_\alpha} = \prod_{\alpha \mathop \in A} x_\alpha$

Proof:
For each $k \in \N_{>0}$, let $\card {B_k} = p_k$.
Let:
:$r_0 = 0$
:$\ds \forall k \in \N_{>0}: r_k = \sum_{j \mathop = 1}^k {p_j}$
and:
:$p = r_n$
Then:
:$r_k - r_{k - 1} = p_k$
So, by Isomorphism to Closed Interval, both integer intervals $\closedint 1 {p_k}$ and $\closedint {r_{k - 1} + 1} {r_k}$ have $p_k$ elements.
By Unique Isomorphism between Equivalent Finite Totally Ordered Sets, there is a unique isomorphism $\tau_k: \closedint 1 {p_k} \to \closedint {r_{k - 1} + 1} {r_k}$ as both are totally ordered.
The orderings on both of these are those induced by the ordering on $\N$.
It is clear that $\tau_k$ is defined as:
:$\forall j \in \closedint 1 {p_k}: \map {\tau_k} j = r_k + j$
For each $k \in \closedint 1 n$, let $\rho_k: \closedint 1 {p_k} \to B_k$ be a bijection.
By Strictly Increasing Sequence induces Partition, the mapping $\sigma: \closedint 1 p \to A$ defined by:
:$\ds \forall j \in \closedint {r_{k - 1} + 1} {r_k}: \forall k \in \closedint 1 n: \map \sigma j = \map {\rho_k} {\map {\tau_k^{-1} } j}$
is a bijection.
Let $\forall j \in \closedint 1 p: y_j = x_{\map \sigma j}$.
By definition:
:$\ds \prod_{\alpha \mathop \in A} {x_\alpha} = \prod_{j \mathop = 1}^p {x_{\map \sigma j} } = \prod_{j \mathop = 1}^p {y_j}$
Also:
:$\ds \forall k \in \closedint 1 n: \prod_{\alpha \mathop \in B_k} {x_\alpha} = \prod_{i \mathop = 1}^{p^k} {x_{\map {\rho_k} i} }$
Also by definition:
:$\ds \prod_{j \mathop = r_{k - 1} + 1}^{r_k} y_j = \prod_{i \mathop = 1}^{p_k} y_{\map {\tau_k} i} = \prod_{i \mathop = 1}^{p_k} x_{\map \sigma {\map {\tau_k} i} } = \prod_{i \mathop = 1}^{p_k} x_{\map {\rho_k} i}$
So by the General Associativity Theorem:
{{begin-eqn}}
{{eqn | l = \prod_{a \mathop \in A} {x_a}
      | r = \prod_{j \mathop = 1}^p y_j
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^n \paren {\prod_{j \mathop = r_{k - 1} \mathop + 1}^{r_k} {y_j} }
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^n \paren {\prod_{i \mathop = 1}^{p_k} x_{\map {\rho_k} i} }
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^n \paren {\prod_{a \mathop \in B_k} x_\alpha}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: External Direct Product of Groups is Group

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups whose identity elements are $e_1$ and $e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the external direct product of $G_1$ and $G_2$.
Then $\struct {G_1 \times G_2, \circ}$ is a group whose identity element is $\tuple {e_1, e_2}$.

Proof:
Taking the group axioms in turn: