avewright/proofwiki-math huggingface dataset:
Theorem: Ordinal is Subset of Successor

Let $x$ and $y$ be ordinals.
Let $y^+$ denote the successor of $y$.
Then:
: $x \subseteq y^+ \iff \left({x \subseteq y \lor x = y^+}\right)$

Proof:
Let $A \subset B$ denote that $A$ is a proper subset of $B$.
Let $A \in B$ denote that $A$ is an element of $B$.
From Transitive Set is Proper Subset of Ordinal iff Element of Ordinal, $\subset$ and $\in$ can be used interchangeably.
Thus:
{{begin-eqn}}
{{eqn | l = x \subseteq y
      | o = \leadsto
      | r = x \subseteq y^+
      | c = Ordinal is Less than Successor
}}
{{eqn | l = x = y^+
      | o = \leadsto
      | r = x \subseteq y^+
      | c = {{Defof|Set Equality|index = 2}}
}}
{{end-eqn}}
Conversely:
{{begin-eqn}}
{{eqn | l = x \subseteq y^+
      | o = \leadsto
      | r = \paren {x \subset y^+ \lor x = y^+}
}}
{{eqn | l = x \subset y^+
      | o = \leadsto
      | r = x \in y^+
      | c = Transitive Set is Proper Subset of Ordinal iff Element of Ordinal
}}
{{eqn | o = \leadsto
      | r = \paren {x = y \lor x \in y}
      | c = {{Defof|Successor Set}}
}}
{{eqn | o = \leadsto
      | r = x \subseteq y
      | c = Transitive Set is Proper Subset of Ordinal iff Element of Ordinal
}}
{{end-eqn}}
{{qed}}
Category:Ordinals
4276m7vd9lj9v2odqtokbhwufap8nx4
Theorem: Indexed Union Equality

Let $A$, $B_x$, and $C_x$ be classes.
Then:
:$\ds \forall x \in A: B_x = C_x \implies \bigcup_{x \mathop \in A} B_x = \bigcup_{x \mathop \in A} C_x$
{{MissingLinks|$\bigcup_{x \mathop \in A} B_x$ and $\bigcup_{x \mathop \in A} C_x$}}

Proof:
Proof follows from Indexed Union Subset and definition of set equality.
{{handwaving}}
Category:Set Union
sd06p7qs0nodpnwpepko0zs1snkr7jq
Theorem: Indexed Union Subset

Let $A$, $B_x$ and $C_x$ be classes.
{{explain|It can be inferred from the context, but the meaning of the subscript on $B_x$ and $C_x$ needs to be explained.}}
Then:
:$\ds \forall x \in A: B_x \subseteq C_x \implies \bigcup_{x \mathop \in A} B_x \subseteq \bigcup_{x \mathop \in A} C_x$
{{MissingLinks|$\bigcup_{x \mathop \in A} B_x$ and $\bigcup_{x \mathop \in A} C_x$}}

Proof:
{{proof wanted}}
Category:Set Union
nnaxj5lt0hhbj4gyixie2ef4rrqsl5e
Theorem: Ordinal is Less than Sum

Let $x$ and $y$ be ordinals.
Then:
:$x \le \paren {x + y}$
:$x \le \paren {y + x}$

Proof:
By Proof by Cases, one of the following holds by Empty Set is Subset of All Sets:
:$\O < y$
:$y = \O$
By Ordinal Addition by Zero:
:$x = \paren {x + \O} = \paren {\O + x}$
By Membership is Left Compatible with Ordinal Addition:
:$\O < y \implies x < \paren {x + y}$
But if $y = \O$, then it is clear the inequality $x \le \paren {x + y}$ holds as well.
So in either case:
:$x \le \paren {x + y}$
Similarly, by Subset is Right Compatible with Ordinal Addition:
:$\O \le y \implies x \le \paren {y + x}$
The fact that $\O \le y$ is clear from Empty Set is Subset of All Sets.
Therefore:
:$x \le \paren {y + x}$
{{qed}}
Category:Ordinal Arithmetic
t42dz17mby1eq0kdrd62nfb2y3tlj70
Theorem: Limit Ordinals Preserved Under Ordinal Addition

Let $x$ and $y$ be ordinals such that $x$ is a limit ordinal.
Then $y + x$ is a limit ordinal.
That is, letting $K_{II}$ denote the class of all limit ordinals:
:$\forall x \in K_{II}: y + x \in K_{II}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = K_{II}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \ne
      | r = \O
      | c = {{Defof|Limit Ordinal}}
}}
{{eqn | ll= \leadsto
      | l = y + x
      | o = \ne
      | r = \O
      | c = Ordinal is Less than Sum
}}
{{eqn | ll= \leadsto
      | l = y + x
      | o = \in
      | r = K_{II}
      | c = {{Defof|Limit Ordinal}}
}}
{{eqn | lo= \lor
      | l = y + x
      | r = z^+
}}
{{end-eqn}}
The result is now obtained by Proof by Contradiction:
{{AimForCont}} $y + x = z^+$.
{{begin-eqn}}
{{eqn | l = y + x
      | r = z^+
}}
{{eqn | ll= \leadsto
      | l = \bigcup_{w \mathop \in x} \paren {y + w}
      | r = z^+
      | c = {{Defof|Ordinal Addition}}
}}
{{eqn | ll= \leadsto
      | l = z
      | o = \in
      | r = \bigcup_{w \mathop \in x} \paren {y + w}
      | c = Ordinal is Less than Successor
}}
{{eqn | ll= \leadsto
      | q = \exists w \in x
      | l = z
      | o = \in
      | r = y + w
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
But $w \in x \implies w^+ \in x$ by Successor of Ordinal Smaller than Limit Ordinal is also Smaller.
{{begin-eqn}}
{{eqn | l = z
      | o = \in
      | r = y + w
}}
{{eqn | ll= \leadsto
      | l = z^+
      | o = \in
      | r = \paren {y + w}^+
      | c = Successor is Less than Successor
}}
{{eqn | ll= \leadsto
      | l = z^+
      | o = \in
      | r = y + w
      | c = {{Defof|Ordinal Addition}}
}}
{{eqn | ll= \leadsto
      | l = z^+
      | o = \in
      | r = z^+ 
      | c = {{Hypothesis}}
}}
{{end-eqn}}
But $z^+ \in z^+$ is clearly a membership loop, and therefore, our assumption must be wrong.
By disjunctive syllogism:
:$y + x \in K_{II}$
{{qed}}
Theorem: Successor is Less than Successor

Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.
Then, $x \in y \iff x^+ \in y^+$.

Proof:
{{begin-eqn}}
{{eqn | l = x \in y
      | o = \implies
      | r = x^+ \in y^+
      | c = Subset is Compatible with Ordinal Successor
}}
{{eqn | l = x \in y
      | o = \impliedby
      | r = x^+ \in y^+
      | c = Sufficient Condition
}}
{{eqn | ll= \leadsto
      | l = x \in y
      | o = \iff
      | r = x^+ \in y^+
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Ordinals
dl020dpt0rt9udh4mh2c4fnnbl1hxv7
Theorem: Successor is Less than Successor

Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.
Then, $x \in y \iff x^+ \in y^+$.

Proof:
Suppose $y^+ \in x^+$.
By the definition of successor, $y^+ \in x \lor y^+ = x$.
Suppose $y^+ = x$.
By Ordinal is Less than Successor, $y \in x$.
Suppose $y^+ \in x$.
By Ordinal is Less than Successor, $y \in y^+$.
By Ordinal is Transitive, $y \in x$.
Theorem: Successor is Less than Successor

Let $x$ and $y$ be ordinals and let $x^+$ denote the successor set of $x$.
Then, $x \in y \iff x^+ \in y^+$.

Proof:
First note that by Successor Set of Ordinal is Ordinal, $x^+$ and $y^+$ are ordinals.
Let $x^+ \in y^+$.
Then since $y^+$ is transitive, $x^+ \subseteq y^+$.
Thus $x \in y$ or $x = y$.
If $x = y$ then $x^+ \in x^+$, contradicting Ordinal is not Element of Itself.
Thus $x \in y$.
Theorem: Ordinal Addition is Associative

Ordinal addition is associative, i.e.:
:$\paren {x + y} + z = x + \paren {y + z}$
holds for all ordinals $x$, $y$ and $z$.

Proof:
By Transfinite Induction on $z$.
Theorem: Derivative of Composite Function/Corollary

:$\dfrac {\d y} {\d x} = \dfrac {\paren {\dfrac {\d y} {\d u} } } {\paren {\dfrac {\d x} {\d u} } }$
for $\dfrac {\d x} {\d u} \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\d y} {\d x} \frac {\d x} {\d u}
      | r = \frac {\d y} {\d u}
      | c = Derivative of Composite Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {\paren {\dfrac {\d y} {\d u} } } {\paren {\dfrac {\d x}{\d u} } }
      | c = dividing both sides by $\dfrac {\d x} {\d u}$
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Subset with Intersection/Corollary

Let $\struct {G, \circ}$ be a group.
Let $X, Y, Z \subseteq G$ such that $X$ is a singleton.
Then:
:$X \circ \paren {Y \cap Z} = \paren {X \circ Y} \cap \paren {X \circ Z}$
:$\paren {Y \cap Z} \circ X = \paren {Y \circ X} \cap \paren {Z \circ X}$
where $X \circ Y$ denotes the subset product of $X$ and $Y$.

Proof:
Let $X = \set x$.
We have from Product of Subset with Intersection that:
: $X \circ \paren {Y \cap Z} \subseteq \paren {X \circ Y} \cap \paren {X \circ Z}$
Let $g \in \paren {X \circ Y} \cap \paren {X \circ Z}$.
Then by definition of subset product:
: $\exists y \in Y, z \in Z: g = x \circ y = x \circ z$
By the Cancellation Laws it follows that $y = z$.
But:
: $g = x \circ y \implies g \in X \circ Y$
: $g = x \circ z \implies g \in X \circ Z$
and so as $x \circ y = x \circ z$ it follows that $g \in X \circ \paren {Y \cap Z}$.
Thus:
: $X \circ \paren {Y \cap Z} \supseteq \paren {X \circ Y} \cap \paren {X \circ Z}$
It follows by definition of set equality that:
:$X \circ \paren {Y \cap Z} = \paren {X \circ Y} \cap \paren {X \circ Z}$
By similar reasoning:
:$\paren {Y \cap Z} \circ X = \paren {Y \circ X} \cap \paren {Z \circ X}$
Hence the result.
{{qed}}
Theorem: Single Instruction URM Programs/Zero Function

The zero function $\Zero: \N \to \N$, defined as:
:$\forall n \in \N: \map \Zero n = 0$

Proof:
The zero function is computed by the following URM program:
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map Z 1$
|}
This sets the value $0$ into $R_1$ and then stops.
The output $0$ is in $R_1$ when the program terminates.
{{qed}}
Category:URM Programs
Category:Primitive Recursive Functions
j8wnk5c37v24jr0wfwo7ehgessgcfj2
Theorem: Single Instruction URM Programs/Successor Function

The successor function $\Succ: \N \to \N$, defined as:
:$\forall n \in \N: \map \Succ n = n + 1$

Proof:
The successor function is computed by the following URM program:
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map S 1$
|}
The input $n$ is in $R_1$ when the program starts.
The program adds $1$ to $r_1$ and then stops.
The output $n + 1$ is in $R_1$ when the program terminates.
{{qed}}
Category:URM Programs
Category:Primitive Recursive Functions
4uvfxbgayev57oipuc6m5u5z7apfukr
Theorem: Single Instruction URM Programs/Projection Function

The projection functions $\pr_j^k: \N^k \to \N$, defined as:
:$\forall j \in \closedint 1 k: \forall \tuple {n_1, n_2, \ldots, n_k} \in \N^k: \map {\pr_j^k} {n_1, n_2, \ldots, n_k} = n_j$

Proof:
The projection functions are computed by the following URM program:
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map C {j, 1}$
|}
The input $\tuple {n_1, n_2, \ldots, n_j, \ldots, n_k}$ is in $R_1, R_2, \ldots, R_j, \ldots, R_k$ when the program starts.
The program copies $r_j$ to $r_1$ and then stops.
The output $n_j$ is in $R_1$ when the program terminates.
{{qed}}
Category:URM Programs
Category:Primitive Recursive Functions
d2vaqix20wd0djv8t6s5w14bb7z4trw
Theorem: Single Instruction URM Programs/Identity Function

The identity function $I_\N: \N \to \N$ defined as:
:$\forall n \in \N: \map {I_\N} n = n$

Proof:
Any of the following URM programs compute the identity function:
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map Z m$
|}
... where $m \ne 1$.
This sets the value $0$ into $R_m$ and then stops.
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map S m$
|}
... where $m \ne 1$.
The input $n$ is in $R_1$ when the program starts.
The program adds $1$ to $r_m$ and then stops.
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map C {j, m}$
|}
... where $m \ne 1$.
The input $n$ is in $R_1$ when the program starts.
The program copies $r_j$ to $r_m$ and then stops.
{|
|-
! align="right" | Line !!
! align="left" | Command
|-
| align="right" | $1$ ||
| align="left" | $\map C {1, 1}$
|}
The input $n$ is in $R_1$ when the program starts.
The program copies $r_1$ to $r_1$, i.e. to itself, and then stops.
In none of these programs is $R_1$ affected, and so no change is effected to the input, which is returned as the output unchanged.
Hence they all compute the identity function.
{{qed}}
Note that the latter program, consisting entirely of $\map C {1, 1}$, is a direct implementation of the projection function program $\pr^1_1: \N \to \N$.
This latter function is the usual way of implementing the identity function as it is well-defined and obvious, and guaranteed to have no other side-effects when embedded in a larger program.
Category:URM Programs
Category:Primitive Recursive Functions
0jn7k38v1kf7jbwljo4ucpxweu161ys
Theorem: Antiassociative Operation has no Idempotent Elements

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\circ$ be antiassociative on $S$.
Then no element of $S$ is idempotent under $ \circ$.
That is:
:$\forall x \in S: x \circ x \ne x$

Proof:
{{AimForCont}} $a \in S$ such that $a$ is idempotent under $\circ$.
That is:
:$a \circ a = a$
Then:
:$\paren {a \circ a} \circ a = a \circ a$ 
and 
:$a \circ \paren {a \circ a} = a \circ a$
This contradicts our assumption that $\circ$ is antiassociative on $S$.
{{qed}}
Category:Antiassociative Structures
octnc43gusmgbg4r2w0mwdtrecxa77v
Theorem: Antiassociative Operation is not Commutative

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\circ$ be antiassociative on $S$.
Then $\circ$ is not commutative on $S$.

Proof:
We will show there are two elements in $S$ that do not commute.
Let $a \in S$.
From Antiassociative Operation has no Idempotent Elements:
:$a \circ a \ne a$
So for some $b \in S$: 
:$a \circ a = b$
Then:
:$\paren {a \circ a} \circ a = b \circ a$
and:
:$a \circ \paren {a \circ a} = a \circ b$
From our assumption, $\circ$ is antiassociative.
So:
:$\paren {a \circ a} \circ a \ne a \circ \paren {a \circ a}$
Hence for some $a, b \in S$:
:$a \circ b \ne b \circ a$
{{qed}}
Category:Antiassociative Structures
oxshi5xc2ba6gf80ayg6w3e9cb7ee27
Theorem: Antiassociative Structure of Finite Order

Let $n \in \N$ such that $n > 2$.
Then there exists an algebraic structure $\struct {S, \circ}$ of order $n$ such that $\circ$ is antiassociative on $S$.

Proof:
Let $S = \set {a_0, \ldots, a_{n - 1} }$.
Let $\circ$ be a binary operation defined on $S$ such that:
:$\forall x \in S: x \circ a_i = a_{\paren {i + 1} \pmod n}$
Then $\forall j, k, m \in \closedint 0 {n - 1}$:
{{begin-eqn}}
{{eqn | l = \paren {a_j \circ a_k} \circ a_m
      | r = a_{\paren {m + 1} \pmod n}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a_j \circ \paren {a_k \circ a_m}
      | r = a_j \circ a_{\paren {m + 1} \pmod n}
}}
{{eqn | r = a_{\paren {m + 2} \pmod n}
}}
{{end-eqn}}
As $n \ge 2$ it follows that:
:$m + 1 \ne m + 2 \pmod n$
and so $\forall j, k, m \in \closedint 0 {n - 1}$:
:$\paren {a_j \circ a_k} \circ a_m \ne a_j \circ \paren {a_k \circ a_m}$
Hence the result.
{{qed}}
Category:Antiassociative Structures
cx9gdmdqgxqy3fe9stoqz7o7ow2x2tp
Theorem: Example:Antiassociative Structure

Let $\struct {\R_{>0}, \circ}$ be an algebraic structure where $\R_{>0}$ denotes the strictly positive real numbers.
Define:
:$\forall x, y \in \R_{>0}: x \circ y = x y + y$
Then $\circ$ is antiassociative on $\R_{>0}$:
:$\forall x, y, z \in \R_{>0}: \paren {x \circ y} \circ z \ne x \circ \paren {y \circ z}$
and so $\struct {\R_{>0}, \circ}$ is an antiassociative structure.

Proof:
Let $a, b, c \in \R_{>0}$:
Then:
{{begin-eqn}}
{{eqn | l = a \circ \paren {b \circ c}
      | r = a \circ \paren {b c + c}
}}
{{eqn | r = a \paren {b c + c} + b c + c
}}
{{eqn | r = a b c + a c + b c + c
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b} \circ c
      | r = \paren {a b + b} \circ c
}}
{{eqn | r = \paren {a b + b} c + c
}}
{{eqn | r = a b c + b c + c
}}
{{end-eqn}}
As $ac \ne 0$:
:$\forall x, y, z \in \R_{>0}: \paren {x \circ y} \circ z \ne x \circ \paren {y \circ z}$
Hence the result.
{{qed}}
Category:Examples of Abstract Algebra
p1xokrft35ar60g9t7hb46492iszobi
Theorem: Reciprocal Sequence is Strictly Decreasing

The reciprocal sequence:
:$\sequence {\operatorname {recip} }: \N_{>0} \to \R$: $n \mapsto \dfrac 1 n$
is strictly decreasing.

Proof:
Follows from Reciprocal Function is Strictly Decreasing and from Restriction of Monotone Function is Monotone.
{{qed}}
Theorem: Reciprocal Sequence is Strictly Decreasing

The reciprocal sequence:
:$\sequence {\operatorname {recip} }: \N_{>0} \to \R$: $n \mapsto \dfrac 1 n$
is strictly decreasing.

Proof:
Let $n \in \N_{>0}$.
{{begin-eqn}}
{{eqn | l = \frac 1 n - \frac 1 {n + 1}
      | r = \frac {\paren {n + 1} - n} {n \paren {n + 1} }
}}
{{eqn | r = \frac 1 {n^2 + n}
}}
{{eqn | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \frac 1 n
      | o = >
      | r = \frac 1 {n + 1}
}}
{{end-eqn}}
Hence the result, as $n$ was arbitrary.
{{qed}}
Theorem: Two-Step Vector Subspace Test

Let $V$ be a vector space over a division ring $K$.
Let $U \subseteq V$ be a non-empty subset of $V$ such that:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall u \in U, \lambda \in K
      | l = \lambda u
      | o = \in
      | r = U
}}
{{eqn | n = 2
      | q = \forall u, v \in U
      | l = u + v
      | o = \in
      | r = U
}}
{{end-eqn}}
Then $U$ is a subspace of $V$.

Proof:
Suppose that $(1)$ and $(2)$ hold.
From $(1)$, we obtain for every $\lambda \in K$ and $u \in U$ that $\lambda u \in U$.
An application of $(2)$ yields the condition of the One-Step Vector Subspace Test.
Hence $U$ is a vector subspace of $V$.
{{qed}}
Theorem: Reciprocal Function is Strictly Decreasing

The reciprocal function:
:$\operatorname{recip}: \R \setminus \set 0 \to \R$, $x \mapsto \dfrac 1 x$
is strictly decreasing:
:on the open interval $\openint 0 \to$
:on the open interval $\openint \gets 0$

Proof:
Let $x \in \openint 0 {+\infty}$.
By the definition of negative powers:
:$\dfrac 1 x = x^{-1}$
From Power Rule for Derivatives:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} x^{-1}
      | r = -x^{-2}
}}
{{end-eqn}}
From Square of Real Number is Non-Negative:
: $-x^{-2} < 0$
for all $x$ within the domain.
Thus from Derivative of Monotone Function, $\operatorname{recip}$ is strictly decreasing.
The proof for $x \in \openint {-\infty} 0$ is similar.
{{qed}}
Theorem: Reciprocal Function is Strictly Decreasing

The reciprocal function:
:$\operatorname{recip}: \R \setminus \set 0 \to \R$, $x \mapsto \dfrac 1 x$
is strictly decreasing:
:on the open interval $\openint 0 \to$
:on the open interval $\openint \gets 0$

Proof:
=== Strictly Increasing on $\openint 0 \to$ ===
Let $a, b \in \Dom {\operatorname {recip} }$ such that $a$ and $b$ are both (strictly) positive.
Let $a < b$.
Then $0 < a < b$.
By Properties of Totally Ordered Field:
:$0 < b^{-1} < a^{-1}$
That is:
:$\dfrac 1 b < \dfrac 1 a$
{{qed|lemma}}
=== Strictly Increasing on $\openint \gets 0$ ===
Let $a, b \in \Dom {\operatorname {recip} }$ such that $a$ and $b$ are both (strictly) negative.
Let $a < b$.
Then $a < b < 0$.
By Inversion Mapping Reverses Ordering in Ordered Group:
:$0 < -b < -a$
By Properties of Totally Ordered Field:
:$0 < \paren {-a}^{-1} < \paren {-b}^{-1}$
By Negative of Product Inverse:
:$\paren {-b}^{-1} = -b^{-1}$
:$\paren {-a}^{-1} = -a^{-1}$
Thus:
:$0 < -a^{-1} < -b^{-1}$
By Inversion Mapping Reverses Ordering in Ordered Group:
:$-\paren {-b^{-1} } < -\paren {-a^{-1} } < 0$
By Inverse of Group Inverse:
:$b^{-1} < a^{-1} < 0$
Thus in particular:
:$\dfrac 1 b < \dfrac 1 a$
{{qed}}
Theorem: Coefficients of Polynomial Product

Let $J$ be a set.
Let $p_1, \ldots p_n$ be polynomial forms in the indeterminates $\set {X_j : j \in J}$ over a commutative ring $R$.
Suppose that for each $i$ with $1 \le i \le n$, we have, for appropriate $a_{i, k} \in R$:
:$p_i = \ds \sum_{k \mathop \in Z} a_{i, k} X^k$
where $Z$ comprises the multiindices of natural numbers over $J$.
Then:
:$\ds \prod_{i \mathop = 1}^n p_i = \sum_{k \mathop \in Z} b_k X^k$
where:
:$\ds b_k := \sum_{k_1 + \cdots + k_n \mathop = k} \paren {\prod_{i \mathop = 1}^n a_{i, k_i} }$

Proof:
We proceed by induction over $n \ge 1$.
Theorem: Subset Product of Subgroups/Necessary Condition

Let $\left({G, \circ}\right)$ be a group.
Let $H, K$ be subgroups of $G$.
Let $H \circ K$ be a subgroup of $G$.
Then $H$ and $K$ are permutable.
That is:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K$ is a subgroup of $G$.
Let $h \circ k \in H \circ K$.
Then $h \circ k$ is the inverse of some element $g$ of $H \circ K$.
Thus we can write $g = h' \circ k'$ for some $h' \in H$ and $k' \in K$.
So:
{{begin-eqn}}
{{eqn | l = h \circ k
      | r = g^{-1}
      | c = Inverse of Group Inverse: $g$ is the inverse of $h \circ k$
}}
{{eqn | r = \paren {h' \circ k'}^{-1}
      | c = 
}}
{{eqn | r = k'^{-1} \circ h'^{-1}
      | c = Inverse of Group Product
}}
{{eqn | o = \in
      | r = K \circ H
      | c = as $K$ and $H$ are both groups
}}
{{end-eqn}}
So by definition of subset:
: $H \circ K \subseteq K \circ H$
Now suppose $x \in K \circ H$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = k \circ h
      | c = for some $k \in K, h \in H$
}}
{{eqn | r = \paren {\paren {k \circ h}^{-1} }^{-1}
      | c = Inverse of Group Inverse
}}
{{eqn | r = \paren {h^{-1} \circ k^{-1} }^{-1}
      | c = Inverse of Group Product
}}
{{eqn | o = \in
      | r = H \circ K
      | c = as $K$ and $H$ are both groups
}}
{{end-eqn}}
So by definition of subset:
:$K \circ H \subseteq H \circ K$
The result follows by definition of set equality.
{{qed}}
Theorem: Subset Product of Subgroups/Necessary Condition

Let $\left({G, \circ}\right)$ be a group.
Let $H, K$ be subgroups of $G$.
Let $H \circ K$ be a subgroup of $G$.
Then $H$ and $K$ are permutable.
That is:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.

Proof:
Suppose $H \circ K$ is a subgroup of $G$.
Then:
{{begin-eqn}}
{{eqn | l = H \circ K
      | r = \paren {H \circ K}^{-1}
      | c = Inverse of Subgroup
}}
{{eqn | r = K^{-1} \circ H^{-1}
      | c = Inverse of Product of Subsets of Group
}}
{{eqn | r = K \circ H
      | c = Inverse of Subgroup
}}
{{end-eqn}}
{{qed}}
Theorem: Subset Product of Subgroups/Sufficient Condition

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Let $H$ and $K$ be permutable subgroups of $G$.
That is, suppose:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.
Then $H \circ K$ is a subgroup of $G$.

Proof:
Suppose $H \circ K = K \circ H$.
First note that $H \circ K \ne \O$, as $e_G = e_G \circ e_G \in H \circ K$, from Identity of Subgroup.
Suppose $a_1, a_2 \in H, b_1, b_2 \in K$.
Then:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} = a_1 \circ \paren {b_1 \circ a_2} \circ b_2$.
Since $H \circ K = K \circ H$, we see that, for some $a \in H, b \in K$:
:$b_1 \circ a_2 = a \circ b$
Thus:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} = \paren {a_1 \circ a} \circ \paren {b \circ b_2}$
As $H, K \le G$, we have $a_1 \circ a \in H$ and $b \circ b_2 \in K$, hence:
:$\paren {a_1 \circ b_1} \circ \paren {a_2 \circ b_2} \in H \circ K$
thus demonstrating closure of $H \circ K$ under $\circ$.
Finally, if $a \circ b \in H \circ K$, then by Inverse of Group Product:
:$\paren {a \circ b}^{-1} = b^{-1} \circ a^{-1}$
Since $b^{-1} \in K$ and $a^{-1} \in H$, we have:
:$\paren {a \circ b}^{-1} \in K \circ H$
and hence $H \circ K$ is shown to be closed under inverses.
Thus, from the Two-Step Subgroup Test, $H \circ K$ is a subgroup of $G$.
{{qed}}
Theorem: Subset Product of Subgroups/Sufficient Condition

Let $\struct {G, \circ}$ be a group.
Let $H, K$ be subgroups of $G$.
Let $H$ and $K$ be permutable subgroups of $G$.
That is, suppose:
:$H \circ K = K \circ H$
where $H \circ K$ denotes subset product.
Then $H \circ K$ is a subgroup of $G$.

Proof:
Suppose $H \circ K = K \circ H$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {H \circ K} \circ \paren {H \circ K}^{-1}
      | r = H \circ K \circ K^{-1} \circ H^{-1}
      | c = Inverse of Product of Subsets of Group
}}
{{eqn | r = H \circ K \circ K \circ H
      | c = Inverse of Subgroup
}}
{{eqn | r = H \circ K \circ H
      | c = Product of Subgroup with Itself
}}
{{eqn | r = H \circ H \circ K
      | c = by hypothesis
}}
{{eqn | r = H \circ K
      | c = Product of Subgroup with Itself
}}
{{end-eqn}}
That is:
:$\paren {H \circ K} \circ \paren {H \circ K}^{-1} = H \circ K$
Thus by definition of set equality:
:$\paren {H \circ K} \circ \paren {H \circ K}^{-1} \subseteq H \circ K$
So from One-Step Subgroup Test using Subset Product:
:$H \circ K \le G$
{{qed}}