avewright/proofwiki-math huggingface dataset:
Theorem: Left Inverse and Right Inverse is Inverse

Let $\struct {S, \circ}$ be a monoid with identity element $e_S$.
Let $x \in S$ such that $x$ has both a left inverse and a right inverse. That is:
:$\exists x_L \in S: x_L \circ x = e_S$
:$\exists x_R \in S: x \circ x_R = e_S$
Then $x_L = x_R$, that is, $x$ has an inverse.
Furthermore, that element is the ''only'' inverse (both right and left) for $x$

Proof:
We note that as $\struct {S, \circ}$ is a monoid, $\circ$ is associative by definition.
{{begin-eqn}}
{{eqn | l = x_L
      | r = x_L \circ e_S
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = x_L \circ \paren {x \circ x_R}
      | c = {{Defof|Right Inverse Element}}
}}
{{eqn | r = \paren {x_L \circ x} \circ x_R
      | c = {{Defof|Associative Operation}}
}}
{{eqn | r = e_S \circ x_R
      | c = {{Defof|Left Inverse Element}}
}}
{{eqn | r = x_R
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Its uniqueness comes from Inverse in Monoid is Unique.
{{qed}}
Theorem: Left and Right Inverses of Product

Let $\struct {S, \circ}$ be a monoid whose identity is $e_S$.
Let $x, y \in S$.
Let:
:$(1): \quad x \circ y$ have a left inverse for $\circ$
:$(2): \quad y \circ x$ have a right inverse for $\circ$.
Then both $x$ and $y$ are invertible for $\circ$.

Proof:
Let $z_L$ be the left inverse of $x \circ y$ and $z_R$ be the right inverse of $y \circ x$. Then:
{{begin-eqn}}
{{eqn | l = z_L \circ \paren {x \circ y}
      | r = e_S
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = \paren {z_L \circ x} \circ y
      | r = e_S
      | c = Associativity of $\circ$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {y \circ x} \circ z_R
      | r = e_S
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = y \circ \paren {x \circ z_R}
      | r = e_S
      | c = Associativity of $\circ$
}}
{{end-eqn}}
Thus $y$ has both a left inverse $z_L \circ x$ and a right inverse $x \circ z_R$.
From Left Inverse and Right Inverse is Inverse:
:$z_L \circ x = x \circ z_R$
and $y$ has an inverse, that is, is invertible.
{{qed|lemma}}
From the above, we have:
{{begin-eqn}}
{{eqn | l = \paren {z_L \circ x} \circ y
      | r = e_S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x \circ z_R} \circ y
      | r = e_S
      | c = Left Inverse and Right Inverse is Inverse
}}
{{eqn | ll= \leadsto
      | l = x \circ \paren {z_R \circ y}
      | r = e_S
      | c = Associativity of $\circ$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y \circ \paren {x \circ z_R}
      | r = e_S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y \circ \paren {z_L \circ x}
      | r = e_S
      | c = Left Inverse and Right Inverse is Inverse
}}
{{eqn | ll= \leadsto
      | l = \paren {y \circ z_L} \circ x
      | r = e_S
      | c = Associativity of $\circ$
}}
{{end-eqn}}
Thus $x$ has both a left inverse $y \circ z_L$ and a right inverse $z_R \circ y$.
From Left Inverse and Right Inverse is Inverse:
:$y \circ z_L = z_R \circ y$
and $x$ has an inverse, that is, is invertible.
{{qed}}
Theorem: Equivalence of Definitions of Self-Inverse

Let $\struct {S, \circ}$ be a monoid whose identity is $e_S$.
Let $x \in S$.
{{TFAE|def = Self-Inverse Element|context = Abstract Algebra}}

Proof:
Let $x \in S$.
{{begin-eqn}}
{{eqn | l = x \circ x
      | r = e_S
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x \circ x} \circ x^{-1}
      | r = e_S \circ x^{-1}
      | c = {{MonoidAxiom|0}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ \paren {x \circ x^{-1} }
      | r = e_S \circ x^{-1}
      | c = {{MonoidAxiom|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ \paren {x \circ x^{-1} }
      | r = x^{-1}
      | c = {{MonoidAxiom|2}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \circ e_S
      | r = x^{-1}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = x^{-1}
      | c = {{MonoidAxiom|2}}
}}
{{end-eqn}}
{{qed}}
Category:Monoids
Category:Inverse Elements
e7vsitvjfowmtz2g3j0wog4m38nro1k
Theorem: Inverse of Identity Element is Itself

Let $\struct {S, \circ}$ be an algebraic structure with an identity element $e$.
Let the inverse of $e$ be $e^{-1}$.
Then:
:$e^{-1} = e$
That is, $e$ is self-inverse.

Proof:
From Identity Element is Idempotent:
:$e \circ e = e$
Hence the result by definition of identity element.
{{qed}}
Theorem: Invertible Element of Associative Structure is Cancellable

Let $\struct {S, \circ}$ be an algebraic structure where $\circ$ is associative.
Let $\struct {S, \circ}$ have an identity element $e_S$.
An element of $\struct {S, \circ}$ which is invertible is also cancellable.

Proof:
Let $a \in S$ be invertible.
Suppose $a \circ x = a \circ y$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = e_S \circ x
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {a^{-1} \circ a} \circ x
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = a^{-1} \circ \paren {a \circ x}
      | c = Associativity of $\circ$
}}
{{eqn | r = a^{-1} \circ \paren {a \circ y}
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {a^{-1} \circ a} \circ y
      | c = Associativity of $\circ$
}}
{{eqn | r = e_S \circ y
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = y
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
A similar argument shows that $x \circ a = y \circ a \implies x = y$.
{{Qed}}
Theorem: Regular Representation of Invertible Element is Permutation

Let $\struct {S, \circ}$ be a monoid.
Let $a \in S$ be invertible.
Then the left regular representation $\lambda_a$ and the right regular representation $\rho_a$ are permutations of $S$.

Proof:
Suppose $a \in \struct {S, \circ}$ is invertible.
A permutation is a bijection from a set to itself.
As $\lambda_a: S \to S$ and $\rho_a: S \to S$ are defined from $S$ to $S$, all we need to do is show that they are bijections.
To do that we can show that they are both injective and surjective.
Theorem: Group is Inverse Semigroup with Identity

A group is an inverse semigroup with an identity.

Proof:
Let $\struct {S, \circ}$ be a group.
Let $a \in S$.
Then:
{{begin-eqn}}
{{eqn | l = e
      | r = a \circ a^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | ll = \leadsto
      | l = e \circ a
      | r = a \circ a^{-1} \circ a
      | c =
}}
{{eqn | ll= \leadsto
      | l = a
      | r = a \circ a^{-1} \circ a
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = e
      | r = a \circ a^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = a^{-1} \circ e
      | r = a^{-1} \circ a \circ a^{-1}
      | c =
}}
{{eqn | ll= \leadsto
      | l = a^{-1}
      | r = a^{-1} \circ a \circ a^{-1}
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Thus the criteria of an inverse semigroup are fulfilled.
{{qed}}
Category:Group Theory
b4x3t0hbii3q44my8as938x7mwipztd
Theorem: Invertible Elements of Monoid form Subgroup of Cancellable Elements

Let $\struct {S, \circ}$ be an monoid whose identity is $e_S$.
Let $C$ be the set of all cancellable elements of $S$.
Let $T$ be the set of all invertible elements of $S$.
Then $\struct {T, \circ}$ is a subgroup of $\struct {C, \circ}$.

Proof:
From Cancellable Elements of Monoid form Submonoid, $\struct {C, \circ}$ is a submonoid of $\struct {S, \circ}$.
Let its identity be $e_C$ (which may or may not be the same as $e_S$).
Let $T$ be the set of all invertible elements of $S$.
From Invertible Element of Monoid is Cancellable, all the invertible elements of $S$ are also all cancellable, so $T \subseteq C$.
Let $x, y \in T$.
Clearly $x^{-1}, y^{-1} \in T$, as if $x, y$ are invertible, then so are their inverses.
Taking the group axioms in turn:
Theorem: Structure Induced by Associative Operation is Associative

Let $\struct {T, \circ}$ be an algebraic structure.
Let $S$ be a set.
Let $\struct {T^S, \oplus}$ be the structure on $T^S$ induced by $\circ$.
Let $\circ$ be associative.
Then the pointwise operation $\oplus$ induced on $T^S$ by $\circ$ is also associative.

Proof:
Let $f, g, h \in T^S$.
Let $\struct {T, \circ}$ be an associative algebraic structure.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {\paren {f \oplus g} \oplus h} } x
      | r = \map {\paren {f \oplus g} } x \circ \map h x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren {\map f x \circ \map g x} \circ \map h x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x \circ \paren {\map g x \circ \map h x}
      | c = $\circ$ is associative
}}
{{eqn | r = \map f x \circ \map {\paren {g \oplus h} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map {\paren {f \oplus \paren {g \oplus h} } } x
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Structure Induced by Commutative Operation is Commutative

Let $\struct {T, \circ}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus}$ be the structure on $T^S$ induced by $\circ$.
Let $\circ$ be a commutative operation.
Then the pointwise operation $\oplus$ induced on $T^S$ by $\circ$ is also commutative.

Proof:
Let $\struct {T, \circ}$ be a commutative algebraic structure.
Let $f, g \in T^S$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \oplus g} } x
      | r = \map f x \circ \map g x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map g x \circ \map f x
      | c = $\circ$ is commutative
}}
{{eqn | r = \map {\paren {g \oplus f} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Induced Structure Identity

Let $\struct {T, \circ}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus}$ be the structure on $T^S$ induced by $\circ$.
Let $e$ be an identity for $\circ$.
Then the constant mapping $f_e: S \to T$ defined as:
:$\forall x \in S: \map {f_e} x = e$
is the identity for the pointwise operation $\oplus$ induced on $T^S$ by $\circ$.

Proof:
Let $\struct {T, \circ}$ be an algebraic structure with an identity $e$.
Let $f \in T^S$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \oplus f_e} } x
      | r = \map f x \circ \map {f_e} x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x \circ e
      | c = {{Defof|Constant Mapping}} $f_e$
}}
{{eqn | r = \map f x
      | c = $e$ is the identity of $\struct {T, \circ}$
}}
{{eqn | r = e \circ \map f x
      | c = $e$ is the identity of $\struct {T, \circ}$
}}
{{eqn | r = \map {f_e} x \circ \map f x
      | c = {{Defof|Constant Mapping}} $f_e$
}}
{{eqn | r = \map {\paren {f \oplus f_e} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Structure Induced by Abelian Group Operation is Abelian Group

Let $\struct {G, \circ}$ be an abelian group whose identity is $e$.
Let $S$ be a set.
Let $\struct {G^S, \oplus}$ be the structure on $G^S$ induced by $\circ$.
Then $\struct {G^S, \oplus}$ is an abelian group.

Proof:
From Structure Induced by Group Operation is Group, $\struct {G^S, \oplus}$ is a group.
From Structure Induced by Commutative Operation is Commutative, so is the pointwise operation it induces on $G^S$.
Hence the result.
{{qed}}
Category:Abelian Groups
Category:Pointwise Operations
gffz66j74cdmaqb4seldfypi6jcr7vr
Theorem: Power Set with Union is Commutative Monoid

Let $S$ be a set and let $\powerset S$ be its power set.
Then $\struct {\powerset S, \cup}$ is a commutative monoid whose identity is $\O$.
The only invertible element of this structure is $\O$.
Thus (except in the degenerate case $S = \O$) $\struct {\powerset S, \cup}$ cannot be a group.

Proof:
From Power Set is Closed under Union:
:$\forall A, B \in \powerset S: A \cup B \in \powerset S$
From Set System Closed under Union is Commutative Semigroup, $\struct {\powerset S, \cup}$ is a commutative semigroup.
From Identity of Power Set with Union, $\O$ acts as the identity of $\struct {\powerset S, \cup}$.
It remains to be shown that only $\O$ has an inverse:
For $T \subseteq S$ to have an inverse under $\cup$, we require $T^{-1} \cup T = \O$.
From this it follows that $T = \O = T^{-1}$.
The result follows by definition of commutative monoid.
{{qed}}
Theorem: Power Set with Intersection is Commutative Monoid

Let $S$ be a set and let $\powerset S$ be its power set.
Then $\struct {\powerset S, \cap}$ is a commutative monoid whose identity is $S$.
The only invertible element of this structure is $S$.
Thus (except in the degenerate case $S = \O$) $\struct {\powerset S, \cap}$ cannot be a group.

Proof:
From Power Set is Closed under Intersection:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
From Set System Closed under Intersection is Commutative Semigroup, $\struct {\powerset S, \cap}$ is a commutative semigroup.
From Identity of Power Set with Intersection, we have that $S$ acts as the identity.
It remains to be shown that only $S$ has an inverse:
For $T \subseteq S$ to have an inverse under $\cap$, we require $T^{-1} \cap T = S$.
From this it follows that $T = S = T^{-1}$.
The result follows by definition of commutative monoid.
{{qed}}
Theorem: Diagonal Relation is Universally Compatible

The diagonal relation $\Delta_S$ on a set $S$ is universally compatible on $S$.

Proof:
{{questionable|It needs to be pointed out that the definition of universally compatible relation may not be correct as such. I will address it when I work up to that chapter in my book.}}
Let $\struct {S, \circ}$ be any algebraic structure.
{{begin-eqn}}
{{eqn | o = 
      | r = x_1 \Delta_S x_2 \land y_1 \Delta_S y_2
      | c = 
}}
{{eqn | o = \leadsto
      | r = x_1 = x_2 \land y_1 = y_2
      | c = {{Defof|Diagonal Relation}}
}}
{{eqn | o = \leadsto
      | r = x_1 \circ y_1 = x_2 \circ y_2
      | c = (consequence of equality)
}}
{{eqn | o = \leadsto
      | r = \paren {x_1 \circ y_1} \mathrel {\Delta_S} \paren {x_2 \circ y_2}
      | c = {{Defof|Diagonal Relation}}
}}
{{end-eqn}}
{{qed}}
Category:Compatible Relations
ojnvc70xbvn21prclaa8r0syi2jyj2l
Theorem: Trivial Relation is Universally Congruent

The trivial relation $\RR = S \times S$ on a set $S$ is universally congruent on $S$.

Proof:
Let $\struct {S, \circ}$ be any algebraic structure which is closed for $\circ$.
By definition of trivial relation:
:$x \in S \land y \in S \implies x \mathrel \RR y$
So:
{{begin-eqn}}
{{eqn | l = x_1, x_2, y_1, y_2
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1 \circ y_1, x_2 \circ y_2
      | o = \in
      | r = S
      | c = {{Defof|Closed Algebraic Structure}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 \circ y_1}
      | o = \RR
      | r = \paren {x_2 \circ y_2}
      | c = {{Defof|Trivial Relation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence Relation is Congruence for Constant Operation

Every equivalence relation is a congruence relation for the constant operation.

Proof:
Let $c \in S$.
By the definition of the constant operation:
:$\forall x, y \in S: x \sqbrk c y = c$
Let $\RR$ be an equivalence relation on $S$.
Every equivalence relation is reflexive, so:
:$c \mathrel \RR c$
So:
{{begin-eqn}}
{{eqn | l = x_1 \mathrel \RR x_2
      | o = \land
      | r = y_1 \mathrel \RR y_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 \sqbrk c y_1}
      | o = \RR
      | r = \paren {x_2 \sqbrk c y_2}
      | c = True Statement is implied by Every Statement
}}
{{end-eqn}}
Hence the result.
{{Qed}}
Theorem: Quotient Structure is Well-Defined

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\RR$ be a congruence relation on $\struct {S, \circ}$.
Let $S / \RR$ be the quotient set of $S$ by $\RR$.
Let $\circ_\RR$ be the operation induced on $S / \RR$ by $\circ$.
Then $\circ_\RR$ is a well-defined operation in the quotient structure $\struct {S / \RR, \circ_\RR}$.

Proof:
{{begin-eqn}}
{{eqn | l = \eqclass {x_1} \RR = \eqclass {x_2} \RR
      | o = \land
      | r = \eqclass {y_1} \RR = \eqclass {y_2} \RR
      | c =
}}
{{eqn | ll= \leadsto
      | l = x_1 \mathop \RR x_2
      | o = \land
      | r = y_1 \mathop \RR y_2
      | c = {{Defof|Equivalence Class}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 \circ y_1}
      | o = \RR
      | r = \paren {x_2 \circ y_2}
      | c = {{Defof|Congruence Relation}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {x_1 \circ y_1} \RR
      | r = \eqclass {x_2 \circ y_2} \RR
      | c = {{Defof|Equivalence Class}}
}}
{{end-eqn}}
{{qed}}
Theorem: Quotient Structure on Subset Product

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\RR$ be a congruence for $\circ$ on $S$.
Then:
:$\forall X, Y \in S / \RR: X \circ_\PP Y \subseteq X \circ_\RR Y$
where:
:$S / \RR$ is the quotient of $S$ by $\RR$
:$\circ_\PP$ is the operation induced on $\powerset S$ by $\circ$
:$\circ_\RR$ is the operation induced on $S / \RR$ by $\circ$

Proof:
By definition of subset product:
:$X \circ_\PP Y = \set {x \circ y: x \in X, y \in Y}$
{{explain|Thus? That is not the definition of $X \circ_\RR Y$}}
Thus:
:$X \circ_\RR Y = \set {x \circ y: x \in X, y \in Y} \cup \set {x \circ y: x \in \eqclass X \RR, y \in \eqclass Y \RR}$
The result follows from Subset of Union.
{{qed}}
Theorem: External Direct Product Closure

Let $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ be algebraic structures.
Let $\struct {S \times T, \circ}$ be the external direct product of $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$.
Then:
:$\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ be closed
{{iff}}:
:$\struct {S \times T, \circ}$ is also closed.

Proof:
=== Sufficient Condition ===
{{:External Direct Product Closure/Sufficient Condition}}{{qed|lemma}}
Theorem: External Direct Product Associativity

Let $\struct {S \times T, \circ}$ be the external direct product of the two algebraic structures $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$.
Then:
:$\circ_1$ and $\circ_2$ are associative
{{iff}}:
:$\circ$ is associative.

Proof:
=== Sufficient Condition ===
{{:External Direct Product Associativity/Sufficient Condition}}{{qed|lemma}}
Theorem: External Direct Product of Semigroups

The external direct product of two semigroups is itself a semigroup.

Proof:
* From External Direct Product Closure, the external direct product of two closed algebraic structures is closed.
* From External Direct Product Associativity, the external direct product of two associative algebraic structures is associative.
The result follows.
{{qed}}
Category:External Direct Products
Category:Semigroups
rfsf6v32dacvqqu1r6yv5sv9suy5fq1
Theorem: External Direct Product Commutativity

Let $\struct {S \times T, \circ}$ be the external direct product of the two algebraic structures $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$.
Then:
:$\circ_1$ and $\circ_2$ are commutative
{{iff}}:
:$\circ$ is commutative.

Proof:
=== Sufficient Condition ===
{{:External Direct Product Commutativity/Sufficient Condition}}{{qed|lemma}}
Theorem: External Direct Product Identity

Let $\struct {S \times T, \circ}$ be the external direct product of two algebraic structures $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$.
Then:
:$\struct {S, \circ_1}$ has identity element $e_S$ and $\struct {T, \circ_2}$ has identity element $e_T$
{{iff}}:
:$\tuple {e_S, e_T}$ is the identity element for $\struct {S \times T, \circ}$.

Proof:
=== Sufficient Condition ===
{{:External Direct Product Identity/Sufficient Condition}}{{qed|lemma}}
Theorem: External Direct Product Inverses

Let $\struct {S \times T, \circ}$ be the external direct product of the two algebraic structures $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$.
Then:
:$s^{-1}$ and $t^{-1}$ are inverse elements of $s \in \struct {S, \circ_1}$ and $t \in \struct {T, \circ_2}$ respectively
{{iff}}:
:$\tuple {s^{-1}, t^{-1} }$ is an inverse element of $\tuple {s, t} \in \struct {S \times T, \circ}$.

Proof:
=== Sufficient Condition ===
{{:External Direct Product Inverses/Sufficient Condition}}{{qed|lemma}}
Theorem: Morphism Property Preserves Closure

Let $\phi: \struct {S, \circ_1, \circ_2, \ldots, \circ_n} \to \struct {T, *_1, *_2, \ldots, *_n}$ be a mapping from one algebraic structure $\struct {S, \circ_1, \circ_2, \ldots, \circ_n}$ to another $\struct {T, *_1, *_2, \ldots, *_n}$.
Let $\circ_k$ have the morphism property under $\phi$ for some operation $\circ_k$ in $\struct {S, \circ_1, \circ_2, \ldots, \circ_n}$.
Then the following properties hold:
:If $S' \subseteq S$ is closed under $\circ_k$, then $\phi \sqbrk {S'}$ is closed under $*_k$
:If $T' \subseteq T$ is closed under $*_k$, then $\phi^{-1} \sqbrk {T'}$ is closed under $\circ_k$
where $\phi \sqbrk {S'}$ denotes the image of $S'$.

Proof:
Suppose that $\circ_k$ has the morphism property under $\phi$.
{{ProofWanted|It remains to be shown that the Theorem is true where S is the empty set <br/>The empty case seems considered, doesn't it?<br/>Please feel free to take this debate to the talk page. I also have no idea why we need explicitly to consider the empty set. Suspect AI.}}
Suppose that $S' \subseteq S$ is closed under $\circ_k$.
Thus, for non-empty $S'$:
:$s_1, s_2 \in S' \implies s_1 \circ_k s_2 \in S'$
Similarly, suppose that  $T' \subseteq T$ is closed under $*_k$.
Thus, non-empty $T'$:
:$t_1, t_2 \in T' \implies t_1 *_k t_2 \in T'$
First we prove that $\phi \sqbrk {S'}$ is closed under $*_k$:
{{begin-eqn}}
{{eqn | l = t_1, t_2
      | o = \in
      | r = \phi \sqbrk {S'}
}}
{{eqn | ll= \leadsto
      | q = \exists s_1 \in S'
      | l = t_1
      | r = \map \phi {s_1}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \land
      | q = \exists s_2 \in S'
      | l = t_2
      | r = \map \phi {s_2}
}}
{{eqn | ll= \leadsto
      | l = t_1 *_k t_2
      | r = \map \phi {s_1} *_k \map \phi {s_2}
      | c =
}}
{{eqn | r = \map \phi {s_1 \circ_k s_2}
      | c = {{Defof|Morphism Property}}
}}
{{eqn | ll= \leadsto
      | l = t_1 *_k t_2
      | o = \in
      | r = \phi \sqbrk {S'}
      | c = $S'$ is closed under $\circ$
}}
{{end-eqn}}
Then we prove that $\phi^{-1} \sqbrk {T'}$ is closed under $\circ_k$:
{{begin-eqn}}
{{eqn | l = s_1, s_2
      | o = \in
      | r = \phi^{-1} \sqbrk {T'}
}}
{{eqn | ll= \leadsto
      | l = \map \phi {s_1}, \map \phi {s_2}
      | o = \in
      | r = T'
      | c = {{Defof|Inverse Mapping}}
}}
{{eqn | l = \map \phi {s_1} *_k \map \phi {s_2}
      | o = \in
      | r = T'
      | c =
}}
{{eqn | ll= \leadsto
      | l = \map \phi {s_1 \circ_k s_2}
      | o = \in
      | r = T'
      | c = {{Defof|Morphism Property}}
}}
{{eqn | ll= \leadsto
      | l = s_1 \circ_k s_2
      | o = \in
      | r = \phi^{-1} \sqbrk {T'}
      | c = {{Defof|Inverse Mapping}}
}}
{{end-eqn}}
{{qed}}