avewright/proofwiki-math huggingface dataset:
Theorem: Surjection iff Right Cancellable/Sufficient Condition

Let $f$ be a mapping which is right cancellable.
Then $f$ is a surjection.

Proof:
Let $f: X \to Y$ be a right cancellable mapping.
Let $Y$ contain exactly one element.
Then by definition $Y$ is a singleton.
From Mapping to Singleton is Surjection it follows that $f$ is a surjection.
So let $Y$ contain at least two elements.
Call those two elements $a$ and $b$, and we note that $a \ne b$.
We define the two mappings $h, k$ as follows:
:<nowiki>$h: Y \to Y: \forall y \in Y: \map h y = \begin{cases}
y & : y \in \Img f \\
a & : y \notin \Img f
\end{cases}$</nowiki>
:<nowiki>$k: Y \to Y: \forall y \in Y: \map k y = \begin{cases}
y & : y \in \Img f \\
b & : y \notin \Img f
\end{cases}$</nowiki>
It is clear that:
:$\forall x \in X: \map h {\map f x} = \map f x = \map k {\map f x}$
and so:
:$h \circ f = k \circ f$
But by hypothesis, $f$ is right cancellable.
Thus $h = k$.
{{AimForCont}} $Y \ne \Img f$.
Then:
:$\Img f \subsetneq Y$
That is:
:$\exists y \in Y: y \notin \Img f$
It follows that:
:$a = \map h y = \map k y = b$
But we posited that $a \ne b$.
From this contradiction we conclude that:
:$Y = \Img f$
So, by definition, $f$ must be a surjection.
Theorem: Absolute Value Function on Integers induces Equivalence Relation

Let $\Z$ be the set of integers.
Let $\RR$ be the relation on $\Z$ defined as:
:$\forall x, y \in \Z: \tuple {x, y} \in \RR \iff \size x = \size y$
where $\size x$ denotes the absolute value of $x$.
Then $\RR$ is an equivalence relation.

Proof:
$\RR$ is shown to be an equivalence relation thus:
Theorem: Absolute Value induces Equivalence not Compatible with Integer Addition

Let $\Z$ be the set of integers.
Let $\RR$ be the relation on $\Z$ defined as:
:$\forall x, y \in \Z: \tuple {x, y} \in \RR \iff \size x = \size y$
where $\size x$ denotes the absolute value of $x$.
Then $\RR$ is not a congruence relation for integer addition.

Proof:
From Absolute Value Function on Integers induces Equivalence Relation, $\RR$ is an equivalence relation.
However, consider that:
{{begin-eqn}}
{{eqn | l = \size {-1} = \size 1
      | o = \leadsto
      | r = -1 \mathop \RR 1
      | c = 
}}
{{eqn | l = \size 2 = \size 2
      | o = \leadsto
      | r = 2 \mathop \RR 2
      | c = 
}}
{{end-eqn}}
By conventional integer addition:
:$-1 + 2 = 1$
while:
:$1 + 2 = 3$
But it does not hold that:
:$\size 1 = \size 3$
Therefore $\RR$ is not a congruence relation for integer addition.
Hence the result, by Proof by Counterexample.
{{qed}}
Theorem: Equivalence Relation is Congruence for Right Operation

Every equivalence relation is a congruence for the right operation $\rightarrow$.

Proof:
Let $\RR$ be an equivalence relation on the structure $\struct {S, \rightarrow}$.
Then:
:$x_1 \rightarrow y_1 = y_1$
:$x_2 \rightarrow y_2 = y_2$
Suppose $x_1 \mathrel \RR x_2 \land y_1 \mathrel \RR y_2$.
It follows directly that:
:$\paren {x_1 \rightarrow y_1} \mathrel \RR \paren {x_2 \rightarrow y_2}$
{{Qed}}
Theorem: Equivalence Relation is Congruence for Left Operation

Every equivalence relation is a congruence for the left operation $\leftarrow$.

Proof:
Let $\RR$ be an equivalence relation on the structure $\struct {S, \leftarrow}$.
Then:
:$x_1 \leftarrow y_1 = x_1$
:$x_2 \leftarrow y_2 = x_2$
Suppose $x_1 \mathrel \RR x_2 \land y_1 \mathrel \RR y_2$.
It follows directly that:
:$\paren {x_1 \leftarrow y_1} \mathrel \RR \paren {x_2 \leftarrow y_2}$
{{Qed}}
Theorem: Left Coset Space forms Partition

The left coset space of $H$ forms a partition of its group $G$, and hence:
{{begin-eqn}}
{{eqn | l = x \equiv^l y \pmod H
      | o = \iff
      | r = x H = y H
}}
{{eqn | l = \neg \paren {x \equiv^l y} \pmod H
      | o = \iff
      | r = x H \cap y H = \O
}}
{{end-eqn}}

Proof:
Follows directly from:
:Left Congruence Modulo Subgroup is Equivalence Relation
:Relation Partitions Set iff Equivalence
{{qed}}
Theorem: Right Coset Space forms Partition

The right coset space of $H$ forms a partition of its group $G$:
{{begin-eqn}}
{{eqn | l = x \equiv^r y \pmod H
      | o = \iff
      | r = H x = H y
}}
{{eqn | l = \neg \paren {x \equiv^r y} \pmod H
      | o = \iff
      | r = H x \cap H y = \O
}}
{{end-eqn}}

Proof:
Follows directly from:
:Right Congruence Modulo Subgroup is Equivalence Relation
:Relation Partitions Set iff Equivalence.
{{qed}}
Theorem: Right Cosets are Equal iff Product with Inverse in Subgroup

Let $H x$ denote the right coset of $H$ by $x$.
Then:
:$H x = H y \iff x y^{-1} \in H$

Proof:
{{begin-eqn}}
{{eqn | l = H x
      | r = H y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \equiv^r
      | r = y \bmod H
      | c = Right Coset Space forms Partition
}}
{{eqn | ll= \leadstoandfrom
      | l = x y^{-1}
      | o = \in
      | r = H
      | c = Equivalent Statements for Congruence Modulo Subgroup
}}
{{end-eqn}}
{{Qed}}
Theorem: Left Cosets are Equal iff Product with Inverse in Subgroup

Let $x H$ denote the left coset of $H$ by $x$.
Then:
:$x H = y H \iff x^{-1} y \in H$

Proof:
{{begin-eqn}}
{{eqn | l = x H
      | r = y H
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \equiv^l
      | r = y \pmod H
      | c = Left Coset Space forms Partition
}}
{{eqn | ll= \leadstoandfrom
      | l = x^{-1} y
      | o = \in
      | r = H
      | c = Equivalent Statements for Congruence Modulo Subgroup
}}
{{end-eqn}}
{{Qed}}
Theorem: Left Congruence Class Modulo Subgroup is Left Coset

Let $\RR^l_H$ be the equivalence defined as left congruence modulo $H$.
The equivalence class $\eqclass g {\RR^l_H}$ of an element $g \in G$ is the left coset $g H$.
This is known as the '''left congruence class of $g \bmod H$'''.

Proof:
Let $x \in \eqclass g {\RR^l_H}$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \eqclass g {\RR^l_H}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = g^{-1} x
      | r = h
      | c = {{Defof|Left Congruence Modulo Subgroup|Left Congruence Modulo $H$}}
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = x
      | r = g h
      | c = Group properties
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = g H
      | c = {{Defof|Left Coset}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass g {\RR^l_H}
      | o = \subseteq
      | r = g H
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Now let $x \in g H$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = g H
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = x
      | r = g h
      | c = {{Defof|Left Coset}}
}}
{{eqn | ll= \leadsto
      | l = g^{-1} x
      | r = h \in H
      | c = Group properties
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \eqclass g {\RR^l_H}
      | c = {{Defof|Left Congruence Modulo Subgroup|Left Congruence Modulo $H$}}
}}
{{eqn | ll= \leadsto
      | r = g H \subseteq \eqclass g {\RR^l_H}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Thus:
:$\eqclass g {\RR^l_H} = g H$
that is, the equivalence class $\eqclass g {\RR^l_H}$ of an element $g \in G$ equals the left coset $g H$.
{{Qed}}
Theorem: Right Congruence Class Modulo Subgroup is Right Coset

Let $\RR^r_H$ be the equivalence defined as right congruence modulo $H$.
The equivalence class $\eqclass g {\RR^r_H}$ of an element $g \in G$ is the right coset $H g$.
This is known as the '''right congruence class of $g \bmod H$'''.

Proof:
Let $x \in \eqclass g {\RR^r_H}$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \eqclass g {\RR^r_H}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = x g^{-1}
      | r = h
      | c = {{Defof|Right Congruence Modulo Subgroup|Right Congruence Modulo $H$}}
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = x
      | r = h g
      | c = Group Properties
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = H g
      | c = {{Defof|Right Coset}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass g {\RR^r_H}
      | o = \subseteq
      | r = H g
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Now let $x \in g H$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = H g
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists h \in H
      | l = x
      | r = h g
      | c = {{Defof|Right Coset}}
}}
{{eqn | ll= \leadsto
      | l = x g^{-1}
      | r = h \in H
      | c = Group Properties
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \eqclass g {\RR^r_H}
      | c = {{Defof|Right Congruence Modulo Subgroup|Right Congruence Modulo $H$}}
}}
{{eqn | ll= \leadsto
      | l = H g
      | o = \subseteq
      | r = \eqclass g {\RR^r_H}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Thus:
:$\eqclass g {\RR^r_H} = H g$
That is, the equivalence class $\eqclass g {\RR^r_H}$ of an element $g \in G$ equals the right coset $g H$.
{{Qed}}
Theorem: Right Congruence Modulo Subgroup is Equivalence Relation

Let $x \equiv^r y \pmod H$ denote the relation that $x$ is right congruent modulo $H$ to $y$
Then the relation $\equiv^r$ is an equivalence relation.

Proof:
Let $G$ be a group whose identity is $e$.
Let $H$ be a subgroup of $G$.
For clarity of expression, we will use the notation:
:$\tuple {x, y} \in \RR^r_H$
for:
:$x \equiv^r y \pmod H$
From the definition of right congruence modulo a subgroup, we have:
:$\RR^r_H = \set {\tuple {x, y} \in G \times G: x y^{-1} \in H}$
We show that $\RR^r_H$ is an equivalence:
Theorem: Group Epimorphism is Isomorphism iff Kernel is Trivial

Let $\struct {G, \oplus}$ and $\struct {H, \odot}$ be groups.
Let $\phi: \struct {G, \oplus} \to \struct {H, \odot}$ be a group epimorphism.
Let $e_G$ and $e_H$ be the identities of $G$ and $H$ respectively.
Let $K = \map \ker \phi$ be the kernel of $\phi$.
Then:
:the epimorphism $\phi$ is an isomorphism
{{iff}}
:$K = \set {e_G}$

Proof:
=== Necessary Condition ===
Let $\phi$ be an isomorphism.
Then by definition $\phi$ is a bijective homomorphism.
Thus by definition of bijection, $\phi$ is an injection.
By definition of injection, there exists exactly one element $x$ of $G$ such that $\map \phi x = e_H$.
From Epimorphism Preserves Identity, that element $x$ is $e_G$:
:$\map \phi {e_G} = e_H$
Thus by definition of kernel:
:$\map \ker \phi = \set {e_G}$
{{qed|lemma}}
=== Sufficient Condition ===
Let $K := \map \ker \phi = \set {e_G}$.
From the Quotient Theorem for Epimorphisms:
:$\RR_\phi$ is compatible with $\oplus$
and thus from Kernel is Normal Subgroup of Domain:
:$K \lhd G$
From Congruence Relation induces Normal Subgroup, $\RR_\phi$ is the equivalence defined by $K$.
Let $\RR_K$ be the congruence modulo $K$ induced by $K$.
Suppose $\map \phi x = \map \phi y$.
Then:
:$x \mathop {\RR_K} y$
as $\RR_\phi = \RR_K$ from Congruence Modulo Subgroup is Equivalence Relation.
Thus by Congruence Class Modulo Subgroup is Coset:
:$x \oplus y^{-1} \in K$
Hence:
:$x \oplus y^{-1} = e_G$
and so:
:$x = y$
Thus $\phi$ is injective.
By definition, an injective epimorphism is a isomorphism.
{{qed}}
Theorem: Group Epimorphism is Isomorphism iff Kernel is Trivial

Let $\struct {G, \oplus}$ and $\struct {H, \odot}$ be groups.
Let $\phi: \struct {G, \oplus} \to \struct {H, \odot}$ be a group epimorphism.
Let $e_G$ and $e_H$ be the identities of $G$ and $H$ respectively.
Let $K = \map \ker \phi$ be the kernel of $\phi$.
Then:
:the epimorphism $\phi$ is an isomorphism
{{iff}}
:$K = \set {e_G}$

Proof:
From Kernel is Trivial iff Group Monomorphism, $\phi$ is a monomorphism {{iff}} $K = \set {e_G}$.
By definition, a group $G$ is an epimorphism is an isomorphism {{iff}} $G$ is also a monomorphism.
Hence the result.
{{qed}}
Theorem: Real Numbers are not Well-Ordered under Conventional Ordering

Let $\struct {\R, \leqslant}$ be the ordered structure consisting of the real numbers under the usual ordering.
Then $\struct {\R, \leqslant}$ is not a well-ordered set.

Proof:
;Proof by Counterexample
Consider the set:
:$A := \set {x \in \R: x > 1}$
Suppose $a$ were the smallest element of $A$.
Then $a > 1$.
But then:
:$1 < \dfrac {a + 1} 2 < a$
and so $a$ has been shown not to be the smallest element of $A$ after all.
Hence $A$ has no smallest element.
Thus there exists a subset of $\R$ which has no smallest element.
Thus $\R$ is not a well-ordered under $\leqslant$.
{{qed}}
Theorem: Supremum is Unique

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a non-empty subset of $S$.
Then $T$ has at most one supremum in $S$.

Proof:
Let $c$ and $c'$ both be suprema of $T$ in $S$.
From the definition of supremum, $c$ and $c'$ are upper bounds of $T$ in $S$.
By that definition:
:$c$ is an upper bound of $T$ in $S$ and $c'$ is a supremum of $T$ in $S$ implies that $c' \preceq c$
:$c'$ is an upper bound of $T$ in $S$ and $c$ is a supremum of $T$ in $S$ implies that $c \preceq c'$.
So:
:$c' \preceq c \land c \preceq c'$
and thus by the antisymmetry of the ordering $\preceq$:
:$c = c'$
{{Qed}}
Theorem: Infimum is Unique

Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a non-empty subset of $S$.
Then $T$ has at most one infimum in $S$.

Proof:
Let $c$ and $c'$ both be infima of $T$ in $S$.
From the definition of infimum, $c$ and $c'$ are lower bounds of $T$ in $S$.
By that definition:
:$c$ is a lower bound of $T$ in $S$ and $c'$ is an infimum of $T$ in $S$ implies that $c \preceq c'$
:$c'$ is a lower bound of $T$ in $S$ and $c$ is an infimum of $T$ in $S$ implies that $c' \preceq c$.
So:
:$c' \preceq c \land c \preceq c'$
and thus by the antisymmetry of the ordering $\preceq$:
:$c = c'$
{{Qed}}
Theorem: Infimum of Subgroups in Lattice

Then:
:$\inf \set {H, K} = H \cap K$

Proof:
Let $H, K \in \mathbb G$.
From Set of Subgroups forms Complete Lattice:
:$\inf \set {H, K} = H \cap K$
{{qed}}
Theorem: Supremum of Subgroups in Lattice

Let either $H$ or $K$ be normal in $G$.
Then:
:$\sup \set {H, K} = H \circ K$
where $H \circ K$ denotes subset product.

Proof:
Recall that Set of Subgroups forms Complete Lattice.
Let $L = \sup \set {H, K}$.
Let either $H$ or $K$ be normal in $G$.
Since $L$ contains $H$ and $K$, then $L$ contains $H \circ K$.
The smallest subgroup of $G$ containing $H$ and $K$ is:
:$\gen {H, K}$
the subgroup generated by $H$ and $K$.
From Subset Product with Normal Subgroup as Generator:
:$\gen {H, K} = H \circ K$
when either $H$ or $K$ is normal.
The result follows.
{{qed}}
Theorem: Lexicographic Order on Pair of Totally Ordered Sets is Total Ordering

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\preccurlyeq_l$ be the lexicographic order on $S_1 \times S_2$''':
:$\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2} \iff \paren {x_1 \prec_1 y_1} \lor \paren {x_1 = y_1 \land x_2 \preccurlyeq_2 y_2}$
Then:
:$\preccurlyeq_l$ is a total ordering on $S_1 \times S_2$
{{iff}}
:both $\preccurlyeq_1$ and $\preccurlyeq_2$ are total orderings.

Proof:
Recall that from Lexicographic Order is Ordering we have that $\struct {S_1 \times S_2, \preccurlyeq_l}$ is an ordered set.
Theorem: Lexicographic Order is Ordering

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\preccurlyeq_l$ be the lexicographic order on $S_1 \times S_2$''':
:$\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2} \iff \paren {x_1 \prec_1 y_1} \lor \paren {x_1 = y_1 \land x_2 \preccurlyeq_2 y_2}$
Then $\preccurlyeq_l$ is an ordering on $S_1 \times S_2$.

Proof:
In the following, $\tuple {x_1, x_2}, \tuple {y_1, y_2}, \tuple {z_1, z_2} \in S_1 \times S_2$.
Checking in turn each of the criteria for an ordering:
Theorem: Lexicographic Order on Pair of Well-Ordered Sets is Well-Ordering

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\preccurlyeq_l$ denote the lexicographic order on $S_1 \times S_2$''':
:$\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2} \iff \tuple {x_1 \prec_1 y_1} \lor \tuple {x_1 = y_1 \land x_2 \preccurlyeq_2 y_2}$
Then:
:$\preccurlyeq_l$ is a well-ordering on $S_1 \times S_2$
{{iff}}
:both $\preccurlyeq_1$ and $\preccurlyeq_2$ are well-orderings.

Proof:
From Lexicographic Order is Ordering we have that $\struct {S_1 \times S_2, \preccurlyeq_l}$ is an ordered set.
Theorem: Powers of Commuting Elements of Monoid Commute

:$\forall m, n \in \N: \paren {\circ^m a} \circ \paren {\circ^n b} = \paren {\circ^n b} \circ \paren {\circ^m a}$

Proof:
Because $\struct {S, \circ}$ is a monoid, it is a fortiori also a semigroup.
From Powers of Commuting Elements of Semigroup Commute:
:$\forall m, n \in \N_{>0}: \paren {\circ^m a} \circ \paren {\circ^n b} = \paren {\circ^n b} \circ \paren {\circ^m a}$
That is:
:$\forall m, n \in \N_{>0}: a^m \circ b^n = b^n \circ a^m$
It remains to be shown that the result holds for the cases where $m = 0$ and $n = 0$.
Let $n \in \N$:
{{begin-eqn}}
{{eqn | l = a^m \circ b^0
      | r = a^m \circ e
      | c = Definition of $b^0$
}}
{{eqn | r = a^m
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = e \circ a^m
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = b^0 \circ a^m
      | c = Definition of $b^0$
}}
{{end-eqn}}
Similarly, let $m \in \N$:
{{begin-eqn}}
{{eqn | l = a^0 \circ b^n
      | r = e \circ b^n
      | c = Definition of $a^0$
}}
{{eqn | r = b^n
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = b^n \circ e
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = b^n \circ a^0
      | c = Definition of $a^0$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a^0 \circ b^0
      | r = e \circ e
      | c = Definition of $a^0$ and $b^0$
}}
{{eqn | r = b^0 \circ a^0
      | c = Definition of $a^0$ and $b^0$
}}
{{end-eqn}}
Thus:
:$a^m \circ b^n = b^n \circ a^m$
holds for $n = 0$ and $m = 0$.
Thus:
:$\forall m, n \in \N: a^m \circ b^n = b^n \circ a^m$
{{qed}}
Theorem: Power of Product of Commuting Elements in Monoid equals Product of Powers

:$\forall n \in \N: \circ^n \paren {a \circ b} = \paren {\circ^n a} \circ \paren {\circ^n b}$

Proof:
Because $\struct {S, \circ}$ is a monoid, it is a fortiori also a semigroup.
From Power of Product of Commuting Elements in Semigroup equals Product of Powers:
:$\forall n \in \N_{>0}: \circ^n \paren {a \circ b} = \paren {\circ^n a} \circ \paren {\circ^n b}$
That is:
:$\forall n \in \N_{>0}: \paren {a \circ b}^n = a^n \circ b^n$
It remains to be shown that the result holds for the cases where $n = 0$.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b}^0
      | r = \circ^0 \paren {a \circ b}
      | c = Definition of $\circ$
}}
{{eqn | r = e
      | c = Definition of $\circ^0$
}}
{{eqn | r = e \circ e
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {\circ^0 a} \circ \paren {\circ^0 b}
      | c = Definition of $\circ^0$
}}
{{eqn | r = a^0 \circ b^0
      | c = Definition of $\circ$
}}
{{end-eqn}}
Thus:
:$\paren {a \circ b}^n = a^n \circ b^n$
holds for $n = 0$.
Thus:
:$\forall n \in \N: \paren {a \circ b}^n = a^n \circ b^n$
{{qed}}
Theorem: Index Laws/Product of Indices/Monoid

Let $\struct {S, \circ}$ be a monoid whose identity element is $e$.
For $a \in S$, let $\circ^n a = a^n$ be the $n$th power of $a$.
Then:
:$\forall m, n \in \N: a^{n m} = \paren {a^n}^m = \paren {a^m}^n$

Proof:
Because $\struct {S, \circ}$ is a monoid, it is a fortiori a semigroup.
Hence, from Index Laws for Semigroup: Product of Indices:
:$\forall m, n \in \N_{>0}: \circ^{n m} a = \circ^m \paren {\circ^n a} = \circ^n \paren {\circ^m a}$
That is:
:$\forall m, n \in \N_{>0}: a^{n m} = \paren {a^n}^m = \paren {a^m}^n$
It remains to be shown that the result holds for the cases where $m = 0$ and $n = 0$.
{{begin-eqn}}
{{eqn | l = n \times 0
      | r = 0
      | c = Zero Element of Multiplication on Numbers
}}
{{eqn | r = 0 \times  m
      | c = Zero Element of Multiplication on Numbers
}}
{{eqn | ll= \leadsto
      | l = \circ^{n \times 0} a
      | r = e
      | c = 
}}
{{eqn | ll= \leadsto
      | r = \circ^{0 \times m} a
      | c = 
}}
{{end-eqn}}
so the condition holds for either $n = 0$ or $m = 0$.
Finally, we also have:
:$\circ^n \paren {\circ^0 a} = e = \circ^0 \paren {\circ^m a}$
:$\circ^0 \paren {\circ^n a} = e = \circ^m \paren {\circ^0 a}$
{{qed}}
Theorem: Cardinality of Proper Subset of Finite Set

Let $A$ and $B$ be finite sets such that $A \subsetneqq B$.
Let $\card B = n$, where $\card {\, \cdot \,}$ denotes cardinality.
Then $\card A < n$.

Proof:
The proof proceeds by the Principle of Mathematical Induction on $n$, the cardinality of $B$.
Let $S$ be the set of $n \in \N$ such that every proper subset of any set with $m$ elements is finite and has (strictly) fewer than $n$ elements.
Theorem: First-Countable Space is Hausdorff iff All Convergent Sequences have Unique Limit

Let $T = \struct {S, \tau}$ be a first-countable topological space.
Then $T$ is Hausdorff {{iff}} all convergent sequences on $T$ have a unique limit.

Proof:
=== Sufficient Condition ===
This is shown in Convergent Sequence in Hausdorff Space has Unique Limit.
Note that it does not require first-countability.
{{qed|lemma}}
Theorem: Topologically Distinguishable Points are Distinct

Let $T = \struct {X, \tau}$ be a topological space.
Let $x, y \in X$ be topologically distinguishable.
Then the singleton sets $\set x$ and $\set y$ are disjoint and so:
:$x \ne y$

Proof:
Let $x$ and $y$ be '''topologically distinguishable'''.
Then either:
:$\exists U \in \tau: x \in U \subseteq N_x \subseteq X: y \notin N_x$
or:
:$\exists V \in \tau: y \in V \subseteq N_y \subseteq X: x \notin N_y$
{{AimForCont}} $x = y$.
Then:
:$\map \neg {\exists U \in \tau: x \in U \subseteq N_x \subseteq X: y \notin N_x}$
and:
:$\map \neg {\exists V \in \tau: y \in V \subseteq N_y \subseteq X: x \notin N_y}$
Hence the result by Proof by Contradiction:
:$x \ne y$
and so by Singleton Equality:
:$\set x \ne \set y$
{{qed}}
Theorem: Restriction of Strict Total Ordering is Strict Total Ordering

Let $\struct {S, \prec}$ be a strict total ordering.
Let $T \subseteq S$.
Let $\prec \restriction_T$ be the restriction of $\prec$ to $T$.
Then $\prec \restriction_T$ is a strict total ordering of $T$.

Proof:
By definition of strict total ordering, $\prec$ is:
:$(1): \quad$ a relation which is transitive and antireflexive 
:$(2): \quad$ a relation which is connected.
By Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering:
:$\prec \restriction_T$ is a strict ordering.
It follows from Restriction of Connected Relation is Connected that:
:$\prec \restriction_T$ is connected.
Thus $\prec \restriction_T$ is a strict ordering which is connected.
So by definition $\prec \restriction_T$ is a strict total ordering of $T$.
{{qed}}