avewright/proofwiki-math huggingface dataset:
Theorem: Supremum of Subset Product in Ordered Group

Let $\struct {G, \circ, \preceq}$ be an ordered group.
Suppose that subsets $A$ and $B$ of $G$ admit suprema in $G$.
Then:
:$\sup \paren {A \circ_\PP B} = \sup A \circ \sup B$
where $\circ_\PP$ denotes subset product.

Proof:
Let $a \in A$, $b \in B$.
Then:
{{begin-eqn}}
{{eqn | l = a \circ b
      | o = \preceq
      | r = \sup A \circ b
      | c = {{Defof|Supremum of Set}}
}}
{{eqn | o = \preceq
      | r = \sup A \circ \sup B
      | c = {{Defof|Supremum of Set}}
}}
{{end-eqn}}
Hence $\sup A \circ \sup B$ is an upper bound for $A \circ_\PP B$.
Suppose that $u$ is an upper bound for $A \circ_\PP B$.
Then:
{{begin-eqn}}
{{eqn | q = \forall b \in B: \forall a \in A
      | l = a \circ b
      | o = \preceq
      | r = u
}}
{{eqn | ll= \leadsto
      | q = \forall b \in B: \forall a \in A
      | l = a
      | o = \preceq
      | r = u \circ b^{-1}
}}
{{eqn | ll= \leadsto
      | q = \forall b \in B
      | l = \sup A
      | o = \preceq
      | r = u \circ b^{-1}
      | c = {{Defof|Supremum of Set}}
}}
{{eqn | ll= \leadsto
      | q = \forall b \in B
      | l = b
      | o = \preceq
      | r = \paren {\sup A}^{-1} \circ u
}}
{{eqn | ll= \leadsto
      | l = \sup B
      | o = \preceq
      | r = \paren {\sup A}^{-1} \circ u
      | c = {{Defof|Supremum of Set}}
}}
{{eqn | ll= \leadsto
      | l = \sup A \circ \sup B
      | o = \preceq
      | r = u
}}
{{end-eqn}}
Therefore:
:$\sup \paren {A \circ_\PP B} = \sup A \circ \sup B$
{{qed}}
Theorem: Fatou's Lemma for Measures

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\sequence {E_n}_{n \mathop \in \N} \in \Sigma$ be a sequence of $\Sigma$-measurable sets.
Then:
:$\ds \map \mu {\liminf_{n \mathop \to \infty} E_n} \le \liminf_{n \mathop \to \infty} \map \mu {E_n}$
where:
:$\ds \liminf_{n \mathop \to \infty} E_n$ is the limit inferior of the $E_n$
:the {{RHS}} limit inferior is taken in the extended real numbers $\overline \R$.

Proof:
Let:
:$\ds E := \liminf_{n \mathop \to \infty} E_n$
Then:
{{begin-eqn}}
{{eqn | l = \map \mu E
      | r = \int \chi_E \rd \mu
      | c = {{Defof|Lebesgue Integral|subdef = Simple Function}}
}}
{{eqn | r = \int \liminf_{n \mathop \to \infty} \chi_{E_n} \rd \mu
      | c = Characteristic Function of Limit Inferior of Sequence of Sets
}}
{{eqn | o = \le
      | r = \liminf_{n \mathop \to \infty} \int \chi_{E_n} \rd \mu
      | c = Fatou's Lemma for Integrals
}}
{{eqn | r = \liminf_{n \mathop \to \infty} \map \mu {E_n}
      | c = {{Defof|Lebesgue Integral|subdef = Simple Function}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Pierre Joseph Louis Fatou|cat = Fatou}}
Theorem: Kernel Transformation of Measure is Measure

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $N: X \times \Sigma \to \overline \R_{\ge0}$ be a kernel.
Then $\mu N: X \to \overline \R$, the kernel transformation of $\mu$, is a measure.

Proof:
From the definition of the kernel transformation of $\mu$, we have: 
:$\ds \map {\paren {\mu N} } E = \int \map N {x, E} \rd \map \mu x$
for each $E \in \Sigma$. 
We verify each of the conditions for a measure in turn.
Theorem: Canonical Injection is Injection

Let $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$ be algebraic structures with identities $e_1, e_2$ respectively.
The canonical injections:
:$\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {S_2, \circ_2} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_2: \map {\inj_2} x = \tuple {e_1, x}$
are injections.

Proof:
Let $x, x' \in S_1$.
Suppose that:
:$\map {\inj_1} x = \map {\inj_1} {x'}$
Then by definition of canonical injection:
:$\tuple {x, e_2} = \tuple {x', e_2}$
By Equality of Ordered Pairs:
:$x = x'$
That is, $\inj_1$ is an injection.
{{qed|lemma}}
Similarly, let $x, x' \in S_2$.
Suppose that:
:$\map {\inj_2} x = \map {\inj_2} {x'}$
Then by definition of canonical injection:
:$\tuple {e_1, x} = \tuple {e_1, x'}$
Again by Equality of Ordered Pairs:
:$x = x'$
That is, $\inj_2$ is an injection.
{{qed|lemma}}
So $\inj_1$ and $\inj_2$ are injections.
{{qed}}
Theorem: Canonical Injection is Injection/General Result

Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$ be algebraic structures with identities $e_1, e_2, \ldots, e_j, \ldots, e_n$ respectively.
The canonical injection:
:$\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$
defined as:
:$\map {\inj_j} x = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n}$
is an injection.

Proof:
Let:
:$x, y \in S_j: \map {\inj_j} x = \map {\inj_j} y$
Then:
:$\tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n} = \tuple {e_1, e_2, \dotsc, e_{j - 1}, y, e_{j + 1}, \dotsc, e_n}$
By Equality of Ordered Tuples, it follows directly that:
:$x = y$
Thus the canonical injections are injective.
{{Qed}}
Theorem: Intermediate Value Theorem (Topology)

Let $X$ be a connected topological space.
Let $\struct {Y, \preceq, \tau}$ be a totally ordered set equipped with the order topology.
Let $f: X \to Y$ be a continuous mapping.
Let $a$ and $b$ are two points of $a, b \in X$ such that:
:$\map f a \prec \map f b$
Let:
:$r \in Y: \map f a \prec r \prec \map f b$
Then there exists a point $c$ of $X$ such that:
:$\map f c = r$

Proof:
Let $a, b \in X$, and let $r \in Y$ lie between $\map f a$ and $\map f b$.
Define the sets:
:$A = f \sqbrk X \cap r^\prec$ and $B = f \sqbrk X \cap r^\succ$
where $r^\prec$ and $r^\succ$ denote the strict lower closure and strict upper closure respectively of $r$ in $Y$.
$A$ and $B$ are disjoint by construction.
$A$ and $B$ are also non-empty since one contains $\map f a$ and the other contains $\map f b$.
$A$ and $B$ are also both open by definition as the intersection of open sets.
{{AimForCont}} there is no point $c$ such that $\map f c = r$.
Then:
:$f \sqbrk X = A \cup B$
so $A$ and $B$ constitute a separation of $X$.
But this contradicts the fact that Continuous Image of Connected Space is Connected.
Hence by Proof by Contradiction:
:$\exists c \in X: \map f c = r$
which is what was to be proved.
{{qed}}
Theorem: Finite Union of Countable Sets is Countable

The union of a finite number of countable sets is countable.

Proof:
Let $S_0, \ldots, S_{n - 1}$ be countable sets.
For $i \in \set {0, \ldots, n - 1}$, let $f_i: \N \to S_i$ be a surjection.
These exist by Surjection from Natural Numbers iff Countable.
Now define $f: \N \to \ds \bigcup_{i \mathop = 0}^{n - 1} S_i$ by:
:$\map f m := \map {f_i} {\floor {\dfrac m n} }$
where:
:$i$ is the unique element of $\set {0, \ldots, n - 1}$ such that $m \equiv i \pmod n$
:$\floor x$ denotes the floor of $x$.
Now let $x \in \ds \bigcup_{i \mathop = 0}^{n - 1} S_i$ be arbitrary.
Let $k$ be the smallest natural number such that $x \in S_k$.
Let $l$ be the smallest natural number such that $\map {f_k} l = x$.
These are guaranteed to exist by definition of set union and surjectivity of $f_k$, respectively.
Then we have:
:$\map f {l n + k} = \map {f_k} {\floor {\dfrac {l n + k} n} } = \map {f_k} l = x$
since $k < n$.
Since $x$ was arbitrary, $f$ is a surjection.
Hence by Surjection from Natural Numbers iff Countable, $\ds \bigcup_{i \mathop = 0}^{n - 1} S_i$ is countable
{{qed}}
Theorem: Binomial Coefficient with Zero

:$\forall r \in \R: \dbinom r 0 = 1$

Proof:
From the definition of binomial coefficients:
:$\dbinom r k = \dfrac {r^{\underline k} } {k!}$ for $k \ge 0$
where $r^{\underline k}$ is the falling factorial.
In turn:
:$\ds x^{\underline k} := \prod_{j \mathop = 0}^{k - 1} \paren {x - j}$
But when $k = 0$, we have:
:$\ds \prod_{j \mathop = 0}^{-1} \paren {x - j} = 1$
as $\ds \prod_{j \mathop = 0}^{-1} \paren {x - j}$ is a vacuous product.
From the definition of the factorial we have that $0! = 1$.
Thus:
:$\forall r \in \R: \dbinom r 0 = 1$
{{qed}}
Theorem: Binomial Coefficient with One

:$\forall r \in \R: \dbinom r 1 = r$

Proof:
From the definition of binomial coefficients:
:$\dbinom r k = \dfrac {r^{\underline k} } {k!}$ for $k \ge 0$
where $r^{\underline k}$ is the falling factorial.
In turn:
:$\ds x^{\underline k} := \prod_{j \mathop = 0}^{k - 1} \paren {x - j}$
But when $k = 1$, we have:
:$\ds \prod_{j \mathop = 0}^0 \paren {x - j} = \paren {x - 0} = x$
So:
:$\forall r \in \R: \dbinom r 1 = r$
{{qed}}
This is completely compatible with the result for natural numbers:
:$\forall n \in \N: \dbinom n 1 = n$
as from the definition:
:$\dbinom n 1 = \dfrac {n!} {1! \ \paren {n - 1}!}$
the result following directly, again from the definition of the factorial where $1! = 1$.
{{qed}}
Theorem: Binomial Coefficient with Self

:$\forall n \in \Z: \dbinom n n = \sqbrk {n \ge 0}$
where $\sqbrk {n \ge 0}$ denotes Iverson's convention.
That is:
:$\forall n \in \Z_{\ge 0}: \dbinom n n = 1$
:$\forall n \in \Z_{< 0}: \dbinom n n = 0$

Proof:
From the definition of binomial coefficient:
:$\dbinom n n = \dfrac {n!} {n! \ \paren {n - n}!} = \dfrac {n!} {n! \ 0!}$
the result following directly from the definition of the factorial, where $0! = 1$.
From N Choose Negative Number is Zero:
:$\forall k \in \Z_{<0}: \dbinom n k = 0$
So for $n < 0$:
:$\dbinom n n = 0$
{{qed}}
Theorem: Binomial Coefficient with Self

:$\forall n \in \Z: \dbinom n n = \sqbrk {n \ge 0}$
where $\sqbrk {n \ge 0}$ denotes Iverson's convention.
That is:
:$\forall n \in \Z_{\ge 0}: \dbinom n n = 1$
:$\forall n \in \Z_{< 0}: \dbinom n n = 0$

Proof:
The case where $n = 1$ can be taken separately.
From Binomial Coefficient with Zero:
:$\dbinom 1 0 = 1$
demonstrating that the result holds for $n = 1$.
Let $n \in \N: n > 1$.
From the definition of binomial coefficients:
:$\dbinom n {n - 1} = \dfrac {n!} {\paren {n - 1}! \paren {n - \paren {n - 1} }!} = \dfrac {n!} {\paren {n - 1}! \ 1!}$
the result following directly from the definition of the factorial.
{{qed}}
Theorem: Binomial Coefficient with Self

:$\forall n \in \Z: \dbinom n n = \sqbrk {n \ge 0}$
where $\sqbrk {n \ge 0}$ denotes Iverson's convention.
That is:
:$\forall n \in \Z_{\ge 0}: \dbinom n n = 1$
:$\forall n \in \Z_{< 0}: \dbinom n n = 0$

Proof:
From Cardinality of Set of Subsets, $\dbinom n {n - 1}$ is the number of combination of things taken $n - 1$ at a time.
Choosing $n - 1$ things from $n$ is the same thing as choosing which $1$ of the elements to be left out.
There are $n$ different choices for that $1$ element.
Therefore there are $n$ ways to choose $n - 1$ things from $n$.
{{qed}}
Theorem: Binomial Coefficient with Two

:$\forall r \in \R: \dbinom r 2 = \dfrac {r \paren {r - 1} } 2$

Proof:
From the definition of binomial coefficients:
:$\dbinom r k = \dfrac {r^{\underline k}} {k!}$ for $k \ge 0$
where $r^{\underline k}$ is the falling factorial.
In turn:
:$\ds x^{\underline k} := \prod_{j \mathop = 0}^{k - 1} \paren {x - j}$
When $k = 2$:
:$\ds \prod_{j \mathop = 0}^1 \paren {x - j} = \frac {\paren {x - 0} \paren {x - 1} } {2!}$
where $2! = 1 \times 2 = 2$.
So:
:$\forall r \in \R: \dbinom r 2 = \dfrac {r \paren {r - 1} } 2$
{{qed}}
Theorem: Sum of Binomial Coefficients over Lower Index/Corollary

:$\ds \forall n \in \Z_{\ge 0}: \sum_{i \mathop \in \Z} \binom n i = 2^n$

Proof:
From the definition of the binomial coefficient, when $i < 0$ and $i > n$ we have $\dbinom n i = 0$.
The result follows directly from Sum of Binomial Coefficients over Lower Index.
{{qed}}
Category:Binomial Coefficients
Category:Sum of Binomial Coefficients over Lower Index
trh9y7tue8se3pozeep849lc8nqh1ss
Theorem: Binomial Theorem/Integral Index

Let $X$ be one of the standard number systems $\N$, $\Z$, $\Q$, $\R$ or $\C$.
Let $x, y \in X$.
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \Z_{\ge 0}
      | l = \paren {x + y}^n
      | r = \sum_{k \mathop = 0}^n \binom n k x^{n - k} y^k
      | c = 
}}
{{eqn | r = x^n + \binom n 1 x^{n - 1} y + \binom n 2 x^{n - 2} y^2 + \binom n 3 x^{n - 3} y^3 + \cdots + \dbinom n n y^n
      | c = 
}}
{{end-eqn}}
where $\dbinom n k$ is $n$ choose $k$.

Proof:
=== Basis for the Induction ===
For $n = 0$ we have:
:$\ds \paren {x + y}^0 = 1 = \binom 0 0 x^{0 - 0} y^0 = \sum_{k \mathop = 0}^0 \binom 0 k x^{0 - k} y^k$
This is the basis for the induction.
Theorem: Binomial Theorem/Ring Theory

Let $\struct {R, +, \odot}$ be a ringoid such that $\struct {R, \odot}$ is a commutative semigroup.
Let $n \in \Z: n \ge 2$.
Then:
:$\ds \forall x, y \in R: \odot^n \paren {x + y} = \odot^n x + \sum_{k \mathop = 1}^{n - 1} \binom n k \paren {\odot^{n - k} x} \odot \paren {\odot^k y} + \odot^n y$
where $\dbinom n k = \dfrac {n!} {k! \ \paren {n - k}!}$ (see Binomial Coefficient).
If $\struct {R, \odot}$ has an identity element $e$, then:
:$\ds \forall x, y \in R: \odot^n \paren {x + y} = \sum_{k \mathop = 0}^n \binom n k \paren {\odot^{n - k} x} \odot \paren {\odot^k y}$

Proof:
First we establish the result for when $\struct {R, \odot}$ has an identity element $e$.
For $n = 0$ we have:
:$\ds \odot^0 \paren {x + y} = e = {0 \choose 0} \paren {\odot^{0 - 0} x} \odot \paren {\odot^0 y} = \sum_{k \mathop = 0}^0 {0 \choose k} x^{0 - k} \odot y^k$
For $n = 1$ we have:
:$\ds \odot^1 \paren {x + y} = \paren {x + y} = {0 \choose 1} \paren {\odot^{1 - 0} x} \odot \paren {\odot^0 y} + {1 \choose 1} \paren {\odot^{1 - 1} x} \odot \paren {\odot^1 y} = \sum_{k \mathop = 0}^1 {1 \choose k} x^{1 - k} \odot y^k$
Theorem: Derivative of Absolute Value Function

Let $\size x$ be the absolute value of $x$ for real $x$.
Then:
:$\dfrac \d {\d x} \size x = \dfrac x {\size x}$
for $x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \size x
      | r = \frac \d {\d x} \sqrt{x^2}
      | c = Square of Real Number is Non-Negative
}}
{{eqn | r = \frac \d {\d x} \paren {x^2}^{\frac 1 2}
}}
{{eqn | r = \frac 1 2 \paren {x^2}^{-\frac 1 2} \cdot 2 x
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \frac x {\sqrt{x^2} }
}}
{{eqn | r = \frac x {\size x}
}}
{{end-eqn}}
{{qed|lemma}}
Now consider $x = 0$.
From the definition of derivative:
{{begin-eqn}}
{{eqn | l = \valueat {\dfrac {\d \size x} {\d x} } {x \mathop = 0}
      | r = \lim_{x \mathop \to 0}\frac {\size x - 0} {x - 0}
}}
{{eqn | r = \begin {cases} \ds \lim_{x \mathop \to 0^+} \dfrac x x & : x > 0 \\ \ds \lim_{x \mathop \to 0^-} \dfrac {-x} x & : x < 0 \end {cases}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \begin {cases} 1 & : x > 0 \\ -1 & : x < 0 \end {cases}
}}
{{end-eqn}}
From Limit iff Limits from Left and Right, the limit does not exist.
{{qed}}
Theorem: Inverse Element in Inverse Completion of Commutative Monoid

Let $\struct {S, \circ}$ be a commutative monoid.
Let $\struct {C, \circ} \subseteq \struct {S, \circ}$ be the subsemigroup of cancellable elements of $\struct {S, \circ}$.
Let $\struct {T, \circ'}$ be an inverse completion of $\struct {S, \circ}$.
Then the inverse of an element of $S$ which is invertible for $\circ$ is also its inverse for $\circ'$.

Proof:
Let the identity of $\struct {S, \circ}$ be $e$.
Let $z$ be the inverse of $y$ for $\circ$:
:$z \circ y = e$
:$y \circ z = e$
From Identity of Inverse Completion of Commutative Monoid:
:$z \circ' y = e$
:$y \circ' z = e$
Hence $z$ is the inverse of $y$ for $\circ'$.
{{qed}}
Theorem: Construction of Inverse Completion/Congruence Relation

The cross-relation $\boxtimes$ is a congruence relation on $\struct {S \times C, \oplus}$.
=== Members of Equivalence Classes ===
{{:Construction of Inverse Completion/Equivalence Relation/Members of Equivalence Classes}}
=== Equivalence Class of Equal Elements ===
{{:Construction of Inverse Completion/Equivalence Relation/Equivalence Class of Equal Elements}}

Proof:
From Semigroup is Subsemigroup of Itself, $\struct {S, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Also from Semigroup is Subsemigroup of Itself, $\struct {C, \circ {\restriction_C} }$ is a subsemigroup of $\struct {C, \circ {\restriction_C} }$.
The result follows from Cross-Relation is Congruence Relation.
{{qed}}
Theorem: Construction of Inverse Completion/Equivalence Relation/Members of Equivalence Classes

$\forall x, y \in S, a, b \in C:$
:$(1): \quad \tuple {x \circ a, a} \boxtimes \tuple {y \circ b, b} \iff x = y$
:$(2): \quad \eqclass {\tuple {x \circ a, y \circ a} } \boxtimes = \eqclass {\tuple {x, y} } \boxtimes$
where $\eqclass {\tuple {x, y} } \boxtimes$ is the equivalence class of $\tuple {x, y}$ under $\boxtimes$.

Proof:
From Cross-Relation is Equivalence Relation we have that $\boxtimes$ is an equivalence relation.
Hence the equivalence class of $\tuple {x, y}$ under $\boxtimes$ is defined for all $\tuple {x, y} \in S \times C$.
From Semigroup is Subsemigroup of Itself, $\struct {S, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Also from Semigroup is Subsemigroup of Itself, $\struct {C, \circ {\restriction_C} }$ is a subsemigroup of $\struct {C, \circ {\restriction_C} }$.
The result follows from Elements of Cross-Relation Equivalence Class.
{{qed}}
Theorem: Construction of Inverse Completion/Equivalence Relation/Equivalence Class of Equal Elements

:$\forall c, d \in C: \tuple {c, c} \boxtimes \tuple {d, d}$

Proof:
From Semigroup is Subsemigroup of Itself, $\struct {S, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Also from Semigroup is Subsemigroup of Itself, $\struct {C, \circ {\restriction_C} }$ is a subsemigroup of $\struct {C, \circ {\restriction_C} }$.
The result follows from Equivalence Class of Equal Elements of Cross-Relation.
{{qed}}
Theorem: Construction of Inverse Completion/Quotient Structure is Commutative Semigroup

:$\struct {T', \oplus'}$ is a commutative semigroup.

Proof:
The quotient epimorphism from $\struct {S \times C, \oplus}$ onto $\struct {T', \oplus'}$ is given by:
:$q_\boxtimes: \struct {S \times C, \oplus} \to \struct {T', \oplus'}: \map {q_\boxtimes} {x, y} = \eqclass {\tuple {x, y} } \boxtimes$
where, by definition:
{{begin-eqn}}
{{eqn | q = \forall \tuple {x_1, y_1}, \tuple {x_2, y_2} \in S \times C
      | o = 
      | r = \map {q_\boxtimes} {\tuple {x_1, y_1} \oplus \tuple {x_2, y_2} }
      | c = 
}}
{{eqn | r = \map {q_\boxtimes} {x_1, y_1} \oplus' \map {q_\boxtimes} {x_2, y_2}
      | c = 
}}
{{end-eqn}}
By Morphism Property Preserves Closure, as $\oplus$ is closed, then so is $\oplus'$.
By Epimorphism Preserves Associativity, as $\oplus$ is associative, then so is $\oplus'$.
By Epimorphism Preserves Commutativity, as $\oplus$ is commutative, then so is $\oplus'$.
Thus $\struct {T', \oplus'}$  is closed, associative and commutative, and therefore a commutative semigroup.
{{Qed}}
Theorem: Construction of Inverse Completion/Quotient Mapping is Injective

Let the mapping $\psi: S \to T'$ be defined as:
:$\forall x \in S: \map \psi x = \eqclass {\tuple {x \circ a, a} } \boxtimes$
Then $\psi: S \to T'$ is an injection, and does not depend on the particular element $a$ chosen.

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi x
      | r = \map \psi y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a \in C
      | l = \eqclass {\tuple {x \circ a, a} } \boxtimes
      | r = \eqclass {\tuple {y \circ a, a} } \boxtimes
      | c = Definition of $\eqclass {\tuple {x, y} } \boxtimes$
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = Construction of Inverse Completion: Members of Equivalence Classes
}}
{{end-eqn}}
The result follows by the definition of injection.
{{Qed}}
Theorem: Construction of Inverse Completion/Quotient Mapping is Monomorphism

The mapping $\psi: S \to T'$ is a monomorphism.

Proof:
We have that this quotient mapping $\psi: S \to T'$ is an injection.
Let $x, y \in S$. Then:
{{begin-eqn}}
{{eqn | l = \map \psi x \oplus' \map \psi y
      | r = \eqclass {\tuple {x \circ a, a} } \boxtimes \oplus' \eqclass {\tuple {y \circ a, a} } \boxtimes
      | c = Definition of $\psi$
}}
{{eqn | r = \eqclass {\tuple {x \circ a, a} \oplus' \tuple {y \circ a, a} } \boxtimes
      | c = Definition of $\oplus'$
}}
{{eqn | r = \eqclass {\tuple {x \circ a \circ y \circ a, a \circ a} } \boxtimes
      | c = Definition of $\boxtimes$
}}
{{eqn | r = \eqclass {\tuple {\paren {x \circ y} \circ \paren {a \circ a}, a \circ a} } \boxtimes
      | c = Commutativity of $\circ$
}}
{{eqn | r = \map \psi {x \circ y}
      | c = as $a \circ a \in C$
}}
{{end-eqn}}
So $\map \psi {x \circ y} = \map \psi x \oplus' \map \psi y$, and the morphism property is proven.
Thus $\psi$ is an injective homomorphism, and so by definition a monomorphism.
{{Qed}}
Theorem: Construction of Inverse Completion/Quotient Mapping to Image is Isomorphism

Let $S'$ be the image $\psi \sqbrk S$ of $S$.
Then $\psi$ is an isomorphism from $S$ onto $S'$.

Proof:
From Quotient Mapping is Monomorphism, $\psi: \struct {S, \circ} \to \struct {S', \oplus'}$ is a monomorphism.
Therefore by definition:
:$\psi$ is a homomorphism
:$\psi$ is an injection.
Because $S'$ is the image of $\psi \sqbrk S$, by Surjection by Restriction of Codomain $\psi$ is a surjection.
Therefore by definition $\psi: S \to S'$ is a bijection.
A bijective homomorphism is an isomorphism.
{{Qed}}
Theorem: Construction of Inverse Completion/Quotient Mapping/Image of Cancellable Elements

The set $C'$ of cancellable elements of the semigroup $S'$ is $\psi \sqbrk C$.

Proof:
We have Morphism Property Preserves Cancellability.
Thus:
:$c \in C \implies \map \psi c \in C'$
So by Image of Subset under Mapping is Subset of Image:
:$\psi \sqbrk C \subseteq C'$
From above, $\psi$ is an isomorphism.
{{explain|Above where?}}
Hence, also from Morphism Property Preserves Cancellability:
:$c' \in C' \implies \map {\psi^{-1} } {c'} \in C$
So by Preimage of Subset is Subset of Preimage:
:$\psi^{-1} \sqbrk {C'} \subseteq C$
Hence by definition of set equality:
:$\psi \sqbrk C = C'$
{{Qed}}
Theorem: Construction of Inverse Completion/Image of Quotient Mapping is Subsemigroup

Let $S'$ be the image $\psi \sqbrk S$ of $S$.
Then $\struct {S', \oplus'}$ is a subsemigroup of $\struct {T', \oplus'}$.

Proof:
We have that $S'$ is the image $\psi \sqbrk S$ of $S$.
For $\struct {S', \oplus'}$ to be a subsemigroup of $\struct {T', \oplus'}$, by Subsemigroup Closure Test we need to show that $\struct {S', \oplus'}$ is closed.
Let $x, y \in S'$.
Then $x = \map \phi {x'}, y = \map \phi {y'}$ for some $x', y' \in S$.
But as $\phi$ is an isomorphism, it obeys the morphism property.
So $x \oplus' y = \map \phi {x'} \oplus' \map \phi {y'} = \map \phi {x' \circ y'}$.
Hence $x \oplus' y$ is the image of $x' \circ y' \in S$ and hence $x \oplus' y \in S'$.
Thus by the Subsemigroup Closure Test, $\struct {S', \oplus'}$ is a subsemigroup of $\struct {T', \oplus'}$
{{Qed}}
Theorem: Construction of Inverse Completion/Identity of Quotient Structure

Let $c \in C$ be arbitrary.
Then:
:$\eqclass {\tuple {c, c} } \boxtimes$
is the identity of $T'$.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x \circ c} \circ y
      | r = x \circ \paren {c \circ y}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x \circ \paren {y \circ c}
      | c = {{Defof|Commutative Semigroup}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {\tuple {x, y} } \boxtimes \oplus' \eqclass {\tuple {c, c} } \boxtimes
      | r = \eqclass {\tuple {x \circ c, y \circ c} } \boxtimes
      | c = Definition of $\oplus'$
}}
{{eqn | r = \eqclass {\tuple {x, y} } \boxtimes
      | c = Cancellability of elements of $C$
}}
{{end-eqn}}
Hence the result, by definition of identity element.
{{Qed}}