avewright/proofwiki-math huggingface dataset:
Theorem: Image of Composite Mapping

Let $f: S \to T$ and $g: R \to S$ be mappings.
Then:
:$\Img {f \circ g} = f \sqbrk {\Img g}$
where:
: $f \circ g$ is the composition of $g$ and $f$
: $\operatorname{Img}$ denotes image
: $f \sqbrk \cdot$ denotes taking image of a subset under $f$.

Proof:
By definition of image:
:$\Img {f \circ g} = \set {t \in T: \exists r \in R: \map {\paren {f \circ g} } r = t}$
and by definition of the image of a subset:
:$f \sqbrk {\Img g} = \set {t \in T: \exists s \in \Img g: \map f s = t}$
which, expanding what it means that $s \in \Img g$, equals:
:$f \sqbrk {\Img g} = \set {t \in T: \exists s \in S: \exists r \in R: \map g r = s \land \map f s = t}$
Now substituting $\map g r = s$ in $\map f s = t$, we obtain:
:$f \sqbrk {\Img g} = \set {t \in T: \exists s \in S: \exists r \in R: \map f {\map g r} = t}$
which is seen to equal the expression for $\Img {f \circ g}$ as soon as $S$ is non-empty.
The remaining case to be checked is thus if $S = \O$.
From Null Relation is Mapping iff Domain is Empty Set, also $R = \O$, so that $f$ and $g$ are empty mappings.
By Image of Empty Set is Empty Set, we conclude:
:$\Img {f \circ g} = \Img g = \O$
and also:
:$f \sqbrk {\Img g} = \O$
which together yield the desired equality.
Hence the result.
{{qed}}
Theorem: Scalar Multiple of Integrable Function is Integrable Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\mu$-integrable function, and let $\lambda \in \R$.
Then $\lambda f: X \to \overline \R$, the pointwise $\lambda$-multiple of $f$, is also $\mu$-integrable.
That is, the space of integrable functions $\LL^1_{\overline \R}$ is closed under pointwise $\R$-scalar multiplication.

Proof:
{{proof wanted|standard machinery}}
Theorem: Idempotent Elements for Integer Multiplication

There are exactly two integers which are idempotent with respect to multiplication:
:$0 \times 0 = 0$
:$1 \times 1 = 1$

Proof:
The integers $\struct {\Z, +, \times}$ form an integral domain.
By definition of integral domain, therefore, the integers form a ring with no (proper) zero divisors.
The result follows from Idempotent Elements of Ring with No Proper Zero Divisors.
{{qed}}
Theorem: Left Distributive Law for Natural Numbers

The operation of multiplication is left distributive over addition on the set of natural numbers $\N$:
:$\forall x, y, n \in \N_{> 0}: n \times \paren {x + y} = \paren {n \times x} + \paren {n \times y}$

Proof:
Let us cast the proposition in the form:
:$\forall a, b, n \in \N_{> 0}: a \times \paren {b + n} = \paren {a \times b} + \paren {a \times n}$
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\forall a, b \in \N_{> 0}: a \times \paren {b + n} = \paren {a \times b} + \paren {a \times n}$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = a \times \paren {b + 1}
      | r = \paren {a \times b} + a
      | c = Axiom $\text B$
}}
{{eqn | r = \paren {a \times b} + \paren {a \times 1}
      | c = Axiom $\text A$
}}
{{end-eqn}}
and so $\map P 1$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\forall a, b \in \N_{> 0}: a \times \paren {b + k} = \paren {a \times b} + \paren {a \times k}$
Then we need to show:
:$\forall a, b \in \N_{> 0}: a \times \paren {b + \paren {k + 1} } = \paren {a \times b} + \paren {a \times \paren {k + 1} }$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = a \times \paren {b + \paren {k + 1} }
      | r = a \times \paren {\paren {b + k} + 1}
      | c = Axiom $\text C$
}}
{{eqn | r = \paren {a \times \paren {b + k} } + a
      | c = Axiom $\text B$
}}
{{eqn | r = \paren {\paren {a \times b} + \paren {a \times k} } + a
      | c = Induction hypothesis
}}
{{eqn | r = \paren {a \times b} + \paren {\paren {a \times k} + a}
      | c = Natural Number Addition is Associative
}}
{{eqn | r = \paren {a \times b} + \paren {a \times \paren {k + 1} }
      | c = Axiom $\text B$
}}
{{end-eqn}}
The result follows by the Principle of Mathematical Induction.
Theorem: Right Distributive Law for Natural Numbers

The operation of multiplication is right distributive over addition on the set of natural numbers $\N_{> 0}$:
:$\forall x, y, n \in \N_{> 0}: \paren {x + y} \times n = \paren {x \times n} + \paren {y \times n}$

Proof:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\forall a, b \in \N_{> 0}: \paren {a + b} \times n = \paren {a \times n} + \paren {b \times n}$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \paren {a + b} \times 1
      | r = a + b
      | c = Axiom $\text A$
}}
{{eqn | r = \paren {a \times 1} + \paren {b \times 1}
      | c = Axiom $\text A$
}}
{{end-eqn}}
and so $\map P 1$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\forall a, b \in \N_{> 0}: \paren {a + b} \times k = \paren {a \times k} + \paren {b \times k}$
Then we need to show:
:$\forall a, b \in \N_{> 0}: \paren {a + b} \times \paren {k + 1} = \paren {a \times \paren {k + 1} } + \paren {b \times \paren {k + 1} }$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {a + b} \times \paren {k + 1}
      | r = \paren {\paren {a + b} \times k} + \paren {a + b}
      | c = Axiom $\text B$
}}
{{eqn | r = \paren {\paren {a \times k} + \paren {b \times k} } + \paren {a + b}
      | c = Induction hypothesis
}}
{{eqn | r = \paren {\paren {a \times k} + a} + \paren {\paren {b \times k} + b}
      | c = Natural Number Addition is Commutative
}}
{{eqn | r = \paren {a \times \paren {k + 1} } + \paren {b \times \paren {k + 1} }
      | c = Axiom $\text B$
}}
{{end-eqn}}
The result follows by the Principle of Mathematical Induction.
Theorem: Standard Machinery

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\LL^1_{\overline \R} } \mu$ be the space of $\mu$-integrable functions.
Let $\map P {f_1, \ldots, f_n}$ be a proposition, where the variables $f_i$ denote $\mu$-measurable functions $f_i: X \to \overline \R$.
Let every occurrence of an $f_i$ be of the form:
:$\ds \int \map \Phi {f_i} \rd \mu$
for a suitable index set $I$ and multilinear mapping $\Phi: \map {\LL^1_{\overline \R} } \mu^I \to \map {\LL^1_{\overline \R} } \mu$.
Denote with $\map \chi \Sigma$ the set of characteristic functions of elements of $\Sigma$, that is:
:$\map \chi \Sigma := \set {\chi_E: X \to \R: E \in \Sigma}$
{{TFAE}}
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall f_1, \ldots, f_n \in \map \chi \Sigma
      | o =
      | r = \map P {f_1, \ldots, f_n}
}}
{{eqn | n = 2
      | q = \forall f_1, \ldots, f_n \in \map {\LL^1_{\overline \R} } \mu
      | o =
      | r = \map P {f_1, \ldots, f_n}
}}
{{end-eqn}}
that is, it suffices to verify $P$ holds for characteristic functions.
{{WIP|Not completely valid as stated; need to restrict to $E$ with $\map \mu E < +\infty$ and impose more conditions on $P$}}

Proof:
{{proof wanted}}
Category:Proof Techniques
Category:Measure Theory
lf6pm67jgqh6a126f0ew3uujbhppymn
Theorem: Third Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \N$.
If:
:$(1): \quad \map P n$ is true for all $n \le d$ for some $d \in \N$
:$(2): \quad \forall m \in \N: \paren {\forall k \in \N, m \le k < m + d: \map P k} \implies \map P {m + d}$
then $\map P n$ is true for all $n \in \N$.

Proof:
Let $A = \set {n \in \N: \map P n}$.
We show that $A$ is an inductive set.
By $(1)$:
:$\forall 1 \le i \le d: i \in A$
Let:
:$\forall x \ge d: \set {1, 2, \dotsc, x} \subset A$
Then by definition of $A$:
:$\forall k \in \N: x - \paren {d - 1} \le k < x + 1: \map P k$
Thus $\map P {x + 1} \implies x + 1 \in A$
Thus $A$ is an inductive set.
Thus by the fifth axiom of Peano:
:$\forall n \in \N: A = \N \implies \map P n$
{{qed}}
{{Proofread}}
Theorem: Cross-Relation is Equivalence Relation

{{Cross-Relation Context Definition}}
Then $\boxtimes$ is an equivalence relation on $\struct {S_1 \times S_2, \oplus}$.

Proof:
=== Reflexivity ===
:$\forall \tuple {x_1, y_1} \in S_1 \times S_2: x_1 \circ y_1 = x_1 \circ y_1 \implies \tuple {x_1, y_1} \boxtimes \tuple {x_1, y_1}$
So $\boxtimes$ is a reflexive relation.
{{qed|lemma}}
Theorem: Cross-Relation on Natural Numbers is Equivalence Relation

Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
The relation $\boxtimes$ defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
is an equivalence relation on $\struct {\N \times \N, \oplus}$.

Proof:
$\boxtimes$ is an instance of a cross-relation.
We also have that Natural Number Addition is Commutative.
The result therefore follows from Cross-Relation is Equivalence Relation.
{{qed}}
Theorem: Equivalence Classes of Cross-Relation on Natural Numbers

Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Then $\eqclass {\tuple {x, y} } \boxtimes$ is the equivalence class of $\tuple {x, y}$ under $\boxtimes$, where:
:$\eqclass {\tuple {x_1, y_1} } \boxtimes = \eqclass {\tuple {x_2, y_2} } \boxtimes \iff \tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2}$
The equivalence class $\eqclass {\tuple {x, y} } \boxtimes$ is more often denoted more simply as $\eqclass {x, y} {}$.

Proof:
We have that $\struct {\N, +}$ is a commutative semigroup from Natural Number Addition is Commutative.
We also have the result Cross-Relation on Natural Numbers is Equivalence Relation.
The result follows from the definition of equivalence class.
{{qed}}
Theorem: Integer Addition is Well-Defined

Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Let $\eqclass {x, y} {}$ denote the equivalence class of $\tuple {x, y}$ under $\boxtimes$.
Let:
:$\paren {\N \times \N} / \boxtimes$
be the quotient set induced by $\boxtimes$.
The operation $\oplus$ on these equivalence classes is well-defined, in the sense that:
{{begin-eqn}}
{{eqn | l = \eqclass {a_1, b_1} {}
      | r = \eqclass {a_2, b_2} {}
      | c = 
}}
{{eqn | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a_1, b_1} {} \oplus \eqclass {c_1, d_1} {}
      | r = \eqclass {a_2, b_2} {} \oplus \eqclass {c_2, d_2} {}
      | c = 
}}
{{end-eqn}}

Proof:
Let $\eqclass {a_1, b_1} {}, \eqclass {a_2, b_2} {}, \eqclass {c_1, d_1} {}, \eqclass {c_2, d_2} {}$ be $\boxtimes$-equivalence classes such that $\eqclass {a_1, b_1} {} = \eqclass {a_2, b_2} {}$ and $\eqclass {c_1, d_1} {} = \eqclass {c_2, d_2} {}$.
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a_1, b_1} {}
      | r = \eqclass {a_2, b_2} {}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{eqn | lo= \land
      | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a_1 + b_2
      | r = a_2 + b_1
      | c = {{Defof|Cross-Relation}}
}}
{{eqn | lo= \land
      | l = c_1 + d_2
      | r = c_2 + d_1
      | c = {{Defof|Cross-Relation}}
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \tuple {a_1 + c_1} + \tuple {b_2 + d_2}
      | r = \tuple {a_1 + b_2} + \tuple {c_1 + d_2}
      | c = Commutativity and Associativity of $+$
}}
{{eqn | r = \tuple {a_2 + b_1} + \tuple {c_2 + d_1}
      | c = from above: $a_1 + b_2 = a_2 + b_1, c_1 + d_2 = c_2 + d_1$
}}
{{eqn | r = \tuple {a_2 + c_2} + \tuple {b_1 + d_1}
      | c = Commutativity and associativity of $+$
}}
{{eqn | ll= \leadsto
      | l = \tuple {a_1 + c_1, b_1 + d_1}
      | o = \boxtimes
      | r = \tuple {a_2 + c_2, b_2 + d_2}
      | c = Definition of $\boxtimes$
}}
{{eqn | ll= \leadsto
      | l = \tuple {\tuple {a_1, b_1} \oplus \tuple {c_1, d_1} }
      | o = \boxtimes
      | r = \tuple {\tuple {a_2, b_2} \oplus \tuple {c_2, d_2} }
      | c = Definition of $\oplus$
}}
{{end-eqn}}
{{qed}}
Theorem: Addition of Cross-Relation Equivalence Classes on Natural Numbers is Cancellable

Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Let $\eqclass {x, y} {}$ denote the equivalence class of $\tuple {x, y}$ under $\boxtimes$.
{{WIP|Introduce the language of the Definition:Quotient Set.}}
The operation $\oplus$ on these equivalence classes is cancellable, in the sense that:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {} \oplus \eqclass {c_1, d_1} {}
      | r = \eqclass {a, b} {} \oplus \eqclass {c_2, d_2} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = 
}}
{{end-eqn}}
and similarly:
{{begin-eqn}}
{{eqn | l = \eqclass {c_1, d_1} {} \oplus \eqclass {a, b} {}
      | r = \eqclass {c_2, d_2} {} \oplus \eqclass {a, b} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {} \oplus \eqclass {c_1, d_1} {}
      | r = \eqclass {a, b} {} \oplus \eqclass {c_2, d_2} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {b, a} {} \oplus \paren {\eqclass {a, b} {} \oplus \eqclass {c_1, d_1} {} }
      | r = \eqclass {b, a} {} \oplus \paren {\eqclass {a, b} {} \oplus \eqclass {c_2, d_2} {} }
      | c = adding $\eqclass {b, a} {}$ to both sides
}}
{{eqn | ll= \leadsto
      | l = \paren {\eqclass {b, a} {} \oplus \eqclass {a, b} {} } \oplus \eqclass {c_1, d_1} {}
      | r = \paren {\eqclass {b, a} {} \oplus \eqclass {a, b} {} } \oplus \eqclass {c_2, d_2} {}
      | c = Integer Addition is Associative
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a + b, a + b} {} \oplus \eqclass {c_1, d_1} {}
      | r = \eqclass {a + b, a + b} {} \oplus \eqclass {c_2, d_2} {}
      | c = Definition of $\oplus$
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = Identity for Addition of Cross-Relation Equivalence Classes on Natural Numbers
}}
{{end-eqn}}
{{qed}}
{{WIP|This progresses the theory for direct implementation of cross-relation on $\N \times \N$. Needs to be linked to the general approach, which is instantiated in the existing analysis of the inverse completion. The latter may be the most general approach.}}
Theorem: Cross-Relation Equivalence Classes on Natural Numbers are Cancellable for Addition

Let $\struct {\N, +}$ be the semigroup of natural numbers under addition.
Let $\struct {\N \times \N, \oplus}$ be the (external) direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
Let $\eqclass {x, y} {}$ denote the equivalence class of $\tuple {x, y}$ under $\boxtimes$.
{{wtd|Introduce the language of the Definition:Quotient Set.}}
The operation $\oplus$ on these equivalence classes is cancellable, in the sense that:
{{begin-eqn}}
{{eqn | l = \eqclass {a_1, b_1} {}
      | r = \eqclass {a_2, b_2} {}
      | c = 
}}
{{eqn | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a_1, b_1} {} \oplus \eqclass {c_1, d_1} {}
      | r = \eqclass {a_2, b_2} {} \oplus \eqclass {c_2, d_2} {}
      | c = 
}}
{{end-eqn}}

Proof:
Let $\eqclass {a_1, b_1} {}, \eqclass {a_2, b_2} {}, \eqclass {c_1, d_1} {}, \eqclass {c_2, d_2} {}$ be $\boxtimes$-equivalence classes such that $\eqclass {a_1, b_1} {} = \eqclass {a_2, b_2} {}$ and $\eqclass {c_1, d_1} {} = \eqclass {c_2, d_2} {}$.
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a_1, b_1} {}
      | r = \eqclass {a_2, b_2} {}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{eqn | lo= \land
      | l = \eqclass {c_1, d_1} {}
      | r = \eqclass {c_2, d_2} {}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a_1 + b_2
      | r = a_2 + b_1
      | c = {{Defof|Cross-Relation}}
}}
{{eqn | lo= \land
      | l = c_1 + d_2
      | r = c_2 + d_1
      | c = {{Defof|Cross-Relation}}
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \paren {a_1 + c_1} + \paren {b_2 + d_2}
      | r = \paren {a_1 + b_2} + \paren {c_1 + d_2}
      | c = Commutativity and associativity of $+$
}}
{{eqn | r = \paren {a_2 + b_1} + \paren {c_2 + d_1}
      | c = from above: $a_1 + b_2 = a_2 + b_1, c_1 + d_2 = c_2 + d_1$
}}
{{eqn | r = \paren {a_2 + c_2} + \paren {b_1 + d_1}
      | c = Commutativity and associativity of $+$
}}
{{eqn | ll= \leadsto
      | l = \tuple {a_1 + c_1, b_1 + d_1}
      | o = \boxtimes
      | r = \tuple {a_2 + c_2, b_2 + d_2}
      | c = Definition of $\boxtimes$
}}
{{eqn | ll= \leadsto
      | l = \paren {\tuple {a_1, b_1} \oplus \tuple {c_1, d_1} }
      | o = \boxtimes
      | r = \paren {\tuple {a_2, b_2} \oplus \tuple {c_2, d_2} }
      | c = Definition of $\oplus$
}}
{{end-eqn}}
{{qed}}
{{wtd|This progresses the theory for direct implementation of cross-relation on $\N \times \N$. Needs to be linked to the general approach, which is instantiated in the existing analysis of the inverse completion. The latter may be the most general approach.}}
Theorem: Cross-Relation is Congruence Relation

{{Cross-Relation Context Definition}}
The cross-relation $\boxtimes$ is a congruence relation on $\struct {S_1 \times S_2, \oplus}$.

Proof:
From Cross-Relation is Equivalence Relation we have that $\boxtimes$ is an equivalence relation.
We now need to show that:
{{begin-eqn}}
{{eqn | l = \tuple {x_1, y_1}
      | o = \boxtimes
      | r = \tuple {x_2, y_2}
      | c = 
}}
{{eqn | lo= \land
      | l = \tuple {u_1, v_1}
      | o = \boxtimes
      | r = \tuple {u_2, v_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\tuple {x_1, y_1} \oplus \tuple {u_1, v_1} }
      | o = \boxtimes
      | r = \paren {\tuple {x_2, y_2} \oplus \tuple {u_2, v_2} }
      | c = 
}}
{{end-eqn}}
First we note that:
{{begin-eqn}}
{{eqn | n = 1
      | l = \tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2}
      | o = \iff
      | r = x_1 \circ y_2 = y_1 \circ x_2
      | c = 
}}
{{eqn | n = 2
      | l = \tuple {u_1, v_1} \boxtimes \tuple {u_2, v_2}
      | o = \iff
      | r = u_1 \circ v_2 = v_1 \circ u_2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \paren {x_1 \circ u_1} \circ \paren {y_2 \circ v_2}
      | r = x_1 \circ \paren {u_1 \circ y_2} \circ v_2
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x_1 \circ \paren {y_2 \circ u_1} \circ v_2
      | c = Commutativity of $\circ$
}}
{{eqn | r = \paren {x_1 \circ y_2} \circ \paren {u_1 \circ v_2}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {y_1 \circ x_2} \circ \paren {v_1 \circ u_2}
      | c = from $(1)$ and $(2)$
}}
{{eqn | r = \paren {x_2 \circ y_1} \circ \paren {u_2 \circ v_1}
      | c = Commutativity of $\circ$
}}
{{eqn | r = x_2 \circ \paren {y_1 \circ u_2} \circ v_1
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x_2 \circ \paren {u_2 \circ y_1} \circ v_1
      | c = Commutativity of $\circ$
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 \circ u_1} \circ \paren {y_2 \circ v_2}
      | r = \paren {x_2 \circ u_2} \circ \paren {y_1 \circ v_1}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = \tuple {x_1 \circ u_1, y_1 \circ v_1}
      | o = \boxtimes
      | r = \tuple {x_2 \circ u_2, y_2 \circ v_2}
      | c = Definition of $\boxtimes$
}}
{{eqn | ll= \leadsto
      | l = \paren {\tuple {x_1, y_1} \oplus \tuple {u_1, v_1} }
      | o = \boxtimes
      | r = \paren {\tuple {x_2, y_2} \oplus \tuple {u_2, v_2} }
      | c = Definition of $\oplus$
}}
{{end-eqn}}
So $\boxtimes$ is a congruence relation on $\struct {S \times C, \oplus}$.
{{Qed}}
Theorem: Elements of Cross-Relation Equivalence Class

{{Cross-Relation Context Definition}}
Let $\eqclass {\tuple {x, y} } \boxtimes$ be the $\boxtimes$-equivalence class of $\tuple {x, y}$, where $\tuple {x, y} \in S_1 \times S_2$.
Then:
$\forall x, y \in S_1, a, b \in S_2:$
:$(1): \quad \eqclass {\tuple {x \circ a, a} } \boxtimes = \eqclass {\tuple {y \circ b, b} } \boxtimes \iff x = y$
:$(2): \quad \eqclass {\tuple {x \circ a, y \circ a} } \boxtimes = \eqclass {\tuple {x, y} } \boxtimes$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = \eqclass {\tuple {x \circ a, a} } \boxtimes
      | r = \eqclass {\tuple {y \circ b, b} } \boxtimes
      | c = 
}}
{{eqn | l = \tuple {x \circ a, a}
      | o = \boxtimes
      | r = \tuple {y \circ b, b}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ a \circ b
      | r = y \circ b \circ a
      | c = Definition of $\boxtimes$
}}
{{eqn | r = y \circ a \circ b
      | c = Commutativity of $\circ$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = y
      | c = Cancellability of $a \circ b$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = \paren {x \circ a} \circ y
      | r = x \circ \paren {a \circ y}
      | c = as $\circ$ is associative
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x \circ a, y \circ a}
      | o = \boxtimes
      | r = \tuple {x, y}
      | c = Definition of $\boxtimes$
}}
{{eqn | ll= \leadstoandfrom
      | l = \eqclass {\tuple {x \circ a, y \circ a} } \boxtimes
      | r = \eqclass {\tuple {x, y} } \boxtimes
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Equivalence Class of Equal Elements of Cross-Relation

{{Cross-Relation Context Definition}}
Then:
:$\forall c, d \in S_1 \cap S_2: \tuple {c, c} \boxtimes \tuple {d, d}$

Proof:
Note that in order for $\tuple {c, c}$ and $\tuple {d, d}$ to be defined, $c$ and $d$ must be in both $S_1$ and $S_2$.
Hence the restriction given:
:$\forall c, d \in S_1 \cap S_2$
Then:
{{begin-eqn}}
{{eqn | q = \forall c, d \in S_1 \cap S_2
      | l = c \circ d
      | r = d \circ c
      | c = Commutativity of $\circ$
}}
{{eqn | ll= \leadsto
      | l = \tuple {c, c}
      | o = \boxtimes
      | r = \tuple {d, d}
      | c = Definition of $\boxtimes$
}}
{{end-eqn}}
Hence the result.
{{Qed}}
Theorem: Length of Concatenation

Let $S$ and $T$ be words, and let $ST$ be their concatenation.
Then:
:$\size {S T}\ = \size S + \size T$
where $\size S$ denotes the length of $S$.

Proof:
Because of the unique readability of $ST$, we can determine for each symbol $s$ that is part of $S T$, whether:
:$s$ is part of $S$
:$s$ is part of $T$
and furthermore, precisely one of these options occurs.
There are $\size S$ symbols in $S$, and $\size T$ symbols in $T$.
In total, then, $S T$ is seen to consist of $\size S + \size T$ symbols.
{{qed}}
Category:Collations
kdtnqklo78lvd6zsvq3j7sdzaucg3ur