avewright/proofwiki-math huggingface dataset:
Theorem: Finite Cyclic Group is Isomorphic to Integers under Modulo Addition

Let $\struct {G, \circ}$ be a finite group whose identity element is $e$.
Then $\struct {G, \circ}$ is cyclic of order $n$ {{iff}} $\struct {G, \circ}$ is isomorphic with the additive group of integers modulo $n$ $\struct {\Z_n, +_n}$.

Proof:
=== Necessary Condition ===
Let $\struct {G, \circ}$ be a cyclic group of order $n$.
From List of Elements in Finite Cyclic Group:
:$G = \set {a^0, a^1, a^2, \ldots, a^n}$
where $a^0 = e, a^1 = a$.
From the definition of integers modulo $n$, $\Z_n$ can be expressed as:
:$\Z_n = \set {\eqclass 0 n, \eqclass 1 n, \ldots, \eqclass {n - 1} n}$
where $\eqclass x n$ is the residue class of $x$ modulo $n$.
Let $\phi: G \to \Z_n$ be the mapping defined as:
:$\forall k \in \set {0, 1, \ldots, n - 1}: \map \phi {a^k} = \eqclass k n$
By its definition it is clear that $\phi$ is a bijection.
Also:
{{begin-eqn}}
{{eqn | l = \map \phi {a^r \circ a^s}
      | r = \map \phi {a^{r + s} }
      | c = Powers of Group Elements: Sum of Indices
}}
{{eqn | r = \eqclass {r + s} n
      | c = Definition of $\phi$
}}
{{eqn | r = \eqclass r n +_n \eqclass s n
      | c = {{Defof|Modulo Addition}}
}}
{{eqn | r = \map \phi {a^r} +_n \map \phi {a^s}
      | c = Definition of $\phi$
}}
{{end-eqn}}
Thus the morphism property of $\phi$ is demonstrated, and $\phi$ is thus a group homomorphism.
By definition, a group isomorphism is a group homomorphism which is also a bijection.
{{qed|lemma}}
Theorem: Parallelogram Law (Inner Product Space)

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space.
Let $\norm \cdot$ be the inner product norm of $\struct {V, \innerprod \cdot \cdot}$. 
Let $f, g \in V$ be arbitrary.
Then:
:$\norm {f + g}^2 + \norm {f - g}^2 = 2 \paren {\norm f^2 + \norm g^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \norm {f + g}^2 + \norm {f - g}^2
      | r = \innerprod {f + g} {f + g} + \innerprod {f - g} {f - g}
      | c = {{Defof|Inner Product Norm}}
}}
{{eqn | r = \innerprod f f + \innerprod f g + \innerprod g f + \innerprod g g + \innerprod f f - \innerprod f g - \innerprod g f + \innerprod g g
      | c = Linearity of Inner Product
}}
{{eqn | r = 2 \innerprod f f + 2 \innerprod g g
}}
{{eqn | r = 2 \paren {\norm f^2 + \norm g^2}
      | c = {{Defof|Inner Product Norm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Unique Point of Minimal Distance to Closed Convex Subset of Hilbert Space

Let $H$ be a Hilbert space, and let $h \in H$.
Let $K \subseteq H$ be a closed, convex, non-empty subset of $H$.
Then there is a unique point $k_0 \in K$ such that:
:$\norm {h - k_0} = \map d {h, K}$
where $d$ denotes distance to a set.

Proof:
Let $\mathbf 0_H$ be the zero of $H$.
Since for every $k \in K$, we have:
:$\map d {h, k} = \norm {h - k} = \map d {\mathbf 0_H, k - h}$
it follows that:
:$\map d {h, K} = \map d {\mathbf 0_H, K - h}$
{{WLOG}}, we may therefore assume that $h = \mathbf 0_H$.
The problem has therefore reduced to finding $k_0 \in K$ such that:
:$\norm {k_0} = \map d {\mathbf 0_H, K} = \inf \set {\norm k : k \in K}$
Let $d = \map d {\mathbf 0_H, K}$.
By definition of infimum, there exists a sequence $\sequence {k_n}_{n \mathop \in \N}$ such that:
:$\ds \lim_{n \mathop \to \infty} \norm {k_n} = d$
By the Parallelogram Law, we have that for all $m, n \in \N$:
:$(1): \quad \norm {\dfrac {k_n - k_m} 2 } = \dfrac 1 2 \paren {\norm {k_n}^2 + \norm {k_m}^2} - \norm {\dfrac {k_n + k_m} 2 }^2$
Since $K$ is convex, $\dfrac {k_n + k_m} 2 \in K$.
Hence:
:$\norm {\dfrac {k_n + k_m} 2 }^2 \ge d^2$
Now given $\epsilon > 0$, choose $N$ such that for all $n \ge N$:
:$\norm {k_n}^2 < d^2 + \epsilon$
From $(1)$, it follows that:
:$\norm {\dfrac {k_n - k_m} 2} < d^2 + \epsilon - d^2 = \epsilon$
and hence that $\sequence {k_n}_{n \mathop \in \N}$ is a Cauchy sequence.
Since $H$ is a Hilbert space and $K$ is closed, it follows that there is a $k_0 \in K$ such that:
:$\ds \lim_{n \mathop \to \infty} k_n = k_0$
From Norm is Continuous, we infer that $\norm {k_0} = d$.
This demonstrates existence of $k_0$.
For uniqueness, suppose that $h_0 \in K$ has $\norm {h_0} = d$.
Since $K$ is convex, it follows that $\dfrac {h_0 + k_0} 2 \in K$.
This implies that $\norm {\dfrac {h_0 + k_0} 2} \ge d$.
Now from the Triangle Inequality:
:$\norm {\dfrac {h_0 + k_0} 2} \le \dfrac {\norm {h_0} + \norm {k_0} } 2 = d$
meaning that $\norm {\dfrac {h_0 + k_0} 2} = d$.
Thus, the Parallelogram Law implies that:
:$d^2 = \norm {\dfrac {h_0 + k_0} 2}^2 = d^2 - \norm {\dfrac {h_0 - k_0} 2}^2$
from which we conclude that $h_0 = k_0$.
{{qed}}
Theorem: Primitive of Reciprocal of Root of a squared minus x squared/Arcsine Form

:$\ds \int \frac {\d x} {\sqrt {a^2 - x^2} } = \arcsin \frac x a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {a^2 - x^2} }
      | r = \int \frac {\d x} {\sqrt {a^2 \paren {1 - \frac {x^2} {a^2} } } } 
      | c = factor $a^2$ out of the radicand
}}
{{eqn | r = \int \frac {\d x} {\sqrt {a^2} \sqrt {1 - \paren {\frac x a}^2} }
      | c = 
}}
{{eqn | r = \frac 1 a \int \frac {\d x} {\sqrt {1 - \paren {\frac x a}^2} }
}}
{{end-eqn}}
Substitute:
:$\sin \theta = \dfrac x a \iff x = a \sin \theta$
for $\theta \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}$.
From Real Sine Function is Bounded and Shape of Sine Function, this substitution is valid for all $x / a \in \openint {-1} 1$.
Then:
{{begin-eqn}}
{{eqn | l = a^2
      | o = > 
      | r = x^2
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | r = \frac {x^2} {a^2}
      | c = dividing both terms by $a^2$
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | r = \paren {\frac x a}^2
      | c = Powers of Group Elements
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | r = \size {\frac x a}
      | c = taking the square root of both terms
}}
{{eqn | ll= \leadstoandfrom
      | l = -1
      | o = <
      | r = \paren {\frac x a} < 1
      | c = Negative of Absolute Value
}}
{{end-eqn}}
so this substitution will not change the domain of the integrand.
Then:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \sin \theta
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = a \cos \theta \frac {\d \theta} {\d x}
      | c = Differentiating {{WRT|Differentiation}} $x$, Derivative of Sine Function, Chain Rule for Derivatives
}}
{{eqn | l = \frac 1 a \int \frac {\d x} {\sqrt {1 - \paren {\frac x a}^2 } }
      | r = \frac 1 a \int \frac {a \cos \theta} {\sqrt {1 - \sin^2 \theta} } \frac {\d \theta} {\d x} \rd x
      | c = from above
}}
{{eqn | r = \frac a a \int \frac {\cos \theta} {\sqrt {1 - \sin^2 \theta} } \rd \theta
      | c = Integration by Substitution
}}
{{eqn | r = \int \frac {\cos \theta} {\sqrt {\cos^2 \theta} } \rd \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\cos \theta} {\size {\cos \theta} } \rd \theta
      | c = 
}}
{{end-eqn}}
We have defined $\theta$ to be in the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$.
From Sine and Cosine are Periodic on Reals, $\cos \theta > 0$ for the entire interval.
Therefore the absolute value is unnecessary, and the integral simplifies to:
{{begin-eqn}}
{{eqn | l = \int \rd \theta
      | r = \theta + C
}}
{{end-eqn}}
As $\theta$ was stipulated to be in the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$:
:$\sin \theta = \dfrac x a \iff \theta = \arcsin \dfrac x a$
The answer in terms of $x$, then, is:
:$\ds \int \frac {\d x} {\sqrt {a^2 - x^2} } = \arcsin \frac x a + C$
{{qed}}
Theorem: Inner Automorphism is Automorphism

Let $G$ be a group.
Let $x \in G$.
Let $\kappa_x$ be the inner automorphism of $x$ in $G$.
Then $\kappa_x$ is an automorphism of $G$.

Proof:
By definition, $\kappa_x: G \to G$ is a mapping defined as:
:$\forall g \in G: \map {\kappa_x} g = x g x^{-1}$
We need to show that $\kappa_x$ is an automorphism.
First we show $\kappa_x$ is a homomorphism.
{{begin-eqn}}
{{eqn | q = \forall g, h \in G
      | l = \map {\kappa_x} g \map {\kappa_x} h
      | r = \paren {x g x^{-1} } \paren {x h x^{-1} }
      | c = Definition of $\kappa_x$
}}
{{eqn | r = x g \paren {x^{-1} x} h x^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = x \paren {g e h} x^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = x \paren {g h} x^{-1}
      | c = {{Group-axiom|2}}
}}
{{eqn | r = \map {\kappa_x} {g h}
      | c = Definition of $\kappa_x$
}}
{{end-eqn}}
Thus the morphism property is demonstrated.
Next we show that $\kappa_x$ is injective.
{{begin-eqn}}
{{eqn | l = \map {\kappa_x} g
      | r = \map {\kappa_x} h
}}
{{eqn | ll= \leadsto
      | l = x g x^{-1}
      | r = x h x^{-1}
      | c = Definition of $\kappa_x$
}}
{{eqn | ll= \leadsto
      | l = g
      | r = h
      | c = Cancellation Laws
}}
{{end-eqn}}
So $\kappa_x$ is injective.
Finally we show that $\kappa_x$ is surjective.
Note that $\forall h \in G: x^{-1} h x \in G$ from fact that $G$ is a group and therefore closed. So:
{{begin-eqn}}
{{eqn | q = \forall h \in G
      | l = \map {\kappa_x} {x^{-1} h x}
      | r = x \paren {x^{-1} h x} x^{-1}
      | c = Definition of $\kappa_x$
}}
{{eqn | r = \paren {x x^{-1} } h \paren {x x^{-1} }
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e h e
      | c = {{Group-axiom|3}}
}}
{{eqn | r = h
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{MissingLinks}}
Thus every element of $G$ is the image of some element of $G$ under $\kappa_x$ (that is, of $x^{-1} h x$), and surjectivity is proved.
Since $\kappa_x$ is injective and surjective, it is bijective.
Since $\kappa_x$ is a homomorphism that is bijective, it is a (group) isomorphism.
Hence, $\kappa_x: G \to G$ is a (group) isomorphism from $G$ to itself, which is by definition, an automorphism of $G$.
{{Qed}}
Theorem: Order of Automorphism Group

Let $G$ be a finite group whose order is greater than $2$.
Let $\Aut G$ be the automorphism group of $G$.
Then the order of $\Aut G$ is greater than $1$.

Proof:
There are $3$ cases, and for each case we find an automorphism that is not the identity automorphism.
Theorem: Characteristic Subgroup is Transitive

Let $G$ be a group.
Let $H$ be a characteristic subgroup of $G$.
Let $K$ be a characteristic subgroup of $H$.
Then $K$ is a characteristic subgroup of $G$.

Proof:
Let $\phi: G \to G$ be a group automorphism.
Since $H$ is a characteristic subgroup of $G$, we have:
:$\phi \sqbrk H = H$
Thus, from Group Homomorphism Preserves Subgroups, $\phi {\restriction_H}$, the restriction of $\phi$ to $H$, is an automorphism of $H$.
Now since $K$ is a characteristic subgroup of $H$, we have that:
:$\phi {\restriction_H} \sqbrk K = K$
but this immediately implies that:
:$\phi \sqbrk K = K$
by definition of the restriction $\phi {\restriction_H}$.
That is, $K$ is a characteristic subgroup of $G$ as well.
{{qed}}
Theorem: Quotient Theorem for Group Homomorphisms

Let $\phi: G \to G'$ be a (group) homomorphism between two groups $G$ and $G'$.
Then $\phi$ can be decomposed into the form:
:$\phi = \alpha \beta \gamma$
where:
:$\alpha: \Img \phi \to G'$ is a monomorphism
:$\beta: G / \map \ker \phi \to \Img \phi$ is an isomorphism
:$\gamma: G \to G / \map \ker \phi$ is an epimorphism.

Proof:
=== Monomorphism ===
The mapping $\alpha$ is identified with the inclusion mapping $i: \Img \phi \to G'$ defined as:
:$\forall x \in \Img \phi: \map i x = x$
From Inclusion Mapping is Monomorphism, it follows that $\alpha$ is a monomorphism.
{{qed|lemma}}
Theorem: Quotient Theorem for Group Homomorphisms

Let $\phi: G \to G'$ be a (group) homomorphism between two groups $G$ and $G'$.
Then $\phi$ can be decomposed into the form:
:$\phi = \alpha \beta \gamma$
where:
:$\alpha: \Img \phi \to G'$ is a monomorphism
:$\beta: G / \map \ker \phi \to \Img \phi$ is an isomorphism
:$\gamma: G \to G / \map \ker \phi$ is an epimorphism.

Proof:
From {{Corollary|Quotient Theorem for Group Homomorphisms|1}}:
:$N \subseteq K$
{{iff}}:
:there exists a group homomorphism $\psi: G / N \to H$ such that $\phi = \psi \circ q_N$
From Surjection if Composite is Surjection, it follows that the group homomorphism $\psi$ is a surjection.
Hence by definition, $\psi$ is an epimorphism.
{{qed}}
Theorem: Quotient Theorem for Group Homomorphisms

Let $\phi: G \to G'$ be a (group) homomorphism between two groups $G$ and $G'$.
Then $\phi$ can be decomposed into the form:
:$\phi = \alpha \beta \gamma$
where:
:$\alpha: \Img \phi \to G'$ is a monomorphism
:$\beta: G / \map \ker \phi \to \Img \phi$ is an isomorphism
:$\gamma: G \to G / \map \ker \phi$ is an epimorphism.

Proof:
Let $e$ be the identity element of $G$.
Let $\RR$ be the congruence relation defined by $N$ in $G$.
Let $\RR_\phi$ be the equivalence relation induced by $\phi$.
From Condition for Existence of Epimorphism from Quotient Structure to Epimorphic Image:
:there exists an epimorphism $\psi$ from $G / N$ to $H$ which satisfies $\psi \circ q_N = \phi$
{{iff}}:
:$\RR \subseteq \RR_\phi$
It remains to be shown that:
:$\RR \subseteq \RR_\phi$
{{iff}}:
:$N \subseteq K$
{{finish}}
Theorem: Inclusion Mapping is Monomorphism

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\struct {T, \circ}$ be an algebraic substructure of $S$.
Let $\iota: T \to S$ be the inclusion mapping from $T$ to $S$.
Then $\iota$ is a monomorphism.

Proof:
We have that the inclusion mapping is an injection.
Now let $x, y \in T$:
{{begin-eqn}}
{{eqn | l = \map \iota {x \circ y}
      | r = x \circ y
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | r = \map \iota x \circ \map \iota y
      | c = {{Defof|Inclusion Mapping}}
}}
{{end-eqn}}
demonstrating that $\iota$ has the morphism property.
So $\iota$ is a homomorphism which is also an injection.
Thus by definition, $\iota$ is a monomorphism.
{{qed}}
Category:Monomorphisms (Abstract Algebra)
Category:Inclusion Mappings
chf87xg440zrl5gjgtnzx8138ar8ujn
Theorem: Function is Odd Iff Inverse is Odd

Let $f$ be an odd real function with an inverse $f^{-1}$.
Then $f^{-1}$ is also odd.

Proof:
First note that we have:
{{begin-eqn}}
{{eqn | l = y
      | r = \map f x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \map {f^{-1} } y
      | c = Image of Element under Inverse Mapping
}}
{{eqn | ll= \leadsto
      | l = -x
      | r = -\map {f^{-1} } y
      | c = Multiply both sides by $-1$
}}
{{eqn-intertext|Then:}}
{{eqn | l = -y 
      | r = \map f {-x}
      | c = {{Defof|Odd Function}}
}}
{{eqn | ll= \leadsto
      | l = \map {f^{-1} } {-y}
      | r = \map {f^{-1} \circ f} {-x}
      | c = because $f^{-1}$ is a mapping 
}}
{{eqn | r = -x
      | c = Composite of Bijection with Inverse is Identity Mapping
}}
{{eqn | r = -\map {f^{-1} } y
      | c = from above
}}
{{end-eqn}}
The result follows by definition of an odd function. 
{{qed}}
Category:Inverse Mappings
Category:Odd Functions
7krz1w2uo2pkcuh8v4xrzgcnmo7cplc
Theorem: Zassenhaus Lemma

Let $G$ be a group.
Let $H_1$ and $H_2$ be subgroups of $G$ such that:
{{begin-eqn}}
{{eqn | l = N_1
      | o = \lhd
      | r = H_1
}}
{{eqn | l = N_2
      | o = \lhd
      | r = H_2
}}
{{end-eqn}}
where $\lhd$ denotes the relation of being a normal subgroup.
Then:
{{begin-eqn}}
{{eqn | l = \frac {N_1 \paren {H_1 \cap H_2} } {N_1 \paren {H_1 \cap N_2} }
      | o = \cong
      | m = \frac {H_1 \cap H_2} {\paren {H_1 \cap N_2} \paren {N_1 \cap H_2} }
      | mo= \cong
      | r = \frac {N_2 \paren {H_1 \cap H_2} } {N_2 \paren {N_1 \cap H_2} }
}}
{{end-eqn}}
where:
:$N_1 \paren {H_1 \cap H_2}$, and so on, denotes subset product
:$\cong$ denotes group isomorphism.

Proof:
In order for the expressions to make sense, the denominators need to be normal subgroups.
This is demonstrated in the following lemmata:
Theorem: Jordan-Hölder Theorem

Let $G$ be a finite group.
Let $\HH_1$ and $\HH_2$ be two composition series for $G$.
Then:
:$\HH_1$ and $\HH_2$ have the same length
:Corresponding factors of $\HH_1$ and $\HH_2$ are isomorphic.

Proof:
By the Schreier-Zassenhaus Theorem, two normal series have refinements of equal length whose factors are isomorphic.
But from the definition of composition series, $\HH_1$ and $\HH_2$ have no proper refinements.
Hence any such refinements must be identical to $\HH_1$ and $\HH_2$ themselves.
{{qed}}
{{Namedfor|Marie Ennemond Camille Jordan|name2 = Otto Ludwig Hölder|cat = Jordan, C|cat2 = Hölder}}
Theorem: Double Orthocomplement is Closed Linear Span

Let $H$ be a Hilbert space.
Let $A \subseteq H$ be a subset of $H$.
Then the following identity holds:
:$\paren {A^\perp}^\perp = \vee A$
Here $A^\perp$ denotes orthocomplementation, and $\vee A$ denotes the closed linear span.

Proof:
From Orthocomplement is Closed Linear Subspace:
:$\paren {A^\perp}^\perp$ is a closed linear subspace of $H$.
Also:
:$\paren {A^\perp}^\perp \supseteq A$
Indeed, for each $a \in A$, we have:
:$\forall a' \in A^\perp : \innerprod a {a'} = 0$
by definition of $A^\perp$.
This also means that:
:$a \in \paren{A^\perp}^\perp$
by definition of $\paren{A^\perp}^\perp$.
Hence:
:$\vee A \subseteq \paren{A^\perp}^\perp$
{{qed|lemma}}
For the converse direction, note:
:$A \subseteq \vee A$
Now apply Orthocomplement Reverses Subset twice:
:$\paren {A^\perp}^\perp \subseteq \paren {\paren {\vee A}^\perp}^\perp$
By Double Orthocomplement of Closed Linear Subspace:
:$\paren{A^\perp}^\perp \subseteq \vee A$
{{qed}}
Theorem: Orthocomplement is Closed Linear Subspace

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space.
Let $A \subseteq V$ be a subset of $V$.
Then the orthocomplement $A^\perp$ of $A$ is a closed linear subspace of $H$.

Proof:
Let $\sequence {x_n} \subset A^\perp$ be a convergent sequence.
Let $x$ be the limit of $\sequence {x_n}$.
Then, by the definition of orthocomplement:
:$\forall n \in \N, y \in A: \innerprod {x_n} y = 0$
Passing to the limit, from Inner Product is Continuous we have:
:$\forall y \in A: \innerprod x y = 0$
So:
:$x \in A^\perp$
This shows that $A^\perp$ is closed.
{{qed}}
Theorem: Linear Subspace Dense iff Zero Orthocomplement

Let $H$ be a Hilbert space.
Let $K$ be a linear subspace of $H$.
Then $K$ is everywhere dense {{iff}} $K^\perp = \paren 0$, where $K^\perp$ is the orthocomplement of $K$, and $\paren 0$ denotes the zero subspace.

Proof:
=== Sufficient Condition ===
Assume that $K$ is everywhere dense.
Let $x \in K^\perp$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = K^\perp
}}
{{eqn | ll= \leadsto
      | q = \forall y \in K
      | l = x
      | o = \perp
      | r = y
}}
{{eqn | ll= \leadsto
      | q = \forall y \in H
      | l = x
      | o = \perp
      | r = y
      | c = as $K$ is everywhere dense, and Inner Product is Continuous
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 0
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Finite Group has Composition Series

Let $G$ be a finite group.
Then $G$ has a composition series.

Proof:
Let $G$ be a finite group whose identity is $e$.
Either $G$ has a proper non-trivial normal subgroup or it does not.
If not, then:
:$\set e \lhd G$
is the composition series for $G$.
Otherwise, $G$ has one or more proper non-trivial normal subgroup.
Of these, one or more will have a maximum order.
Select one of these and call it $G_1$.
Again, either $G_1$ has a proper non-trivial normal subgroup or it does not.
If not, then:
:$\set e \lhd G_1 \lhd G$
is a composition series for $G$.
By the Jordan-Hölder Theorem, there can be no other composition series which is longer.
As $G_1$ is a proper subgroup of $G$:
:$\order {G_1} < \order G$
where $\order G$ denotes the order of $G$.
Again, if $G_1$ has one or more proper non-trivial normal subgroup, one or more will have a maximum order.
Select one of these and call it $G_2$.
Thus we form a normal series:
:$\set e \lhd G_2 \lhd G_1 \lhd G$
The process can be repeated, and at each stage a normal subgroup is added to the series of a smaller 
order than the previous one.
This process cannot continue infinitely.
Eventually a $G_n$ will be encountered which has no proper non-trivial normal subgroup.
{{Finish|Proof or explanation is required for why the repeated process cannot continue indefinitely. In particular, explain why eventually there will be no non-trivial normal subgroup<br/>Seriously? You need it explained why reducing the size of a finite number cannot go on for ever>?}}
Thus a composition series:
:$\set e \lhd G_n \cdots \lhd G_2 \lhd G_1 \lhd G$
will be the result.
{{qed}}
Theorem: Finite Group has Composition Series

Let $G$ be a finite group.
Then $G$ has a composition series.

Proof:
{{WIP|Bring up to site standards}}
Let $G$ be a finite group whose identity is $e_G$.
We shall use induction on $|G|$.  
If $G$ is trivial ($|G|=1$), then its composition series is 
:$G=\{e_G\}$. 
Suppose $G$ has a composition series if $|G|<n$, then it suffices to construct a composition series for $G$ with order $n$. 
If $G$ is simple, then its composition series is 
:$G\supsetneq \{e_G\}$. 
Otherwise, $G$ has one or more proper non-trivial normal subgroup. Let $S$ denote the set of all non-trivial normal proper subgroup of $G$. 
Notice that $S$ is non-empty, ordered by inclusion, and $G$ is an upper bound of every chain in $S$, then by Zorn's lemma, $S$ has at least one maximal element, denoted $H$. 
Since $H\in S$, $H$ is a non-trivial normal proper subgroup of $G$, in particular, $|H|<|G|$, so by the induction hypothesis, $H$ has a composition series. 
Now we have 
:$G\supsetneq H\supsetneq H_1\supsetneq \cdots \supsetneq H_n\supsetneq \{e_G\}$. 
In order to show that it is indeed a composition series of $G$, it suffices to check that $G/H$ is simple, which is a direct consequence of the maximal property of $H$, so we are done. {{qed}}
Theorem: Length of Subgroup Plus Length of Quotient Group

Let $G$ be a finite group.
Let $H$ be a normal subgroup of $G$.
Then:
:$\map l G = \map l H + \map l {G / H}$
where:
:$\map l G$ denotes the length of $G$
:$G / H$ denotes the quotient group of $G$ by $H$.

Proof:
Let $\HH$ be a composition series of $H$:
:$\set e = H_0 \subset H_1 \subset \dots \subset H_m = H$,
We can construct a composition series $\GG$ for $G$ which contains $H$:
:$\set e = H_0 \subset H_1 \subset \dots \subset H_m = H = G_0 \subset G_1 \subset \dots \subset G_n = G$
where, for $k = 0, \dots, n - 1$:
:$G_k \vartriangleleft G_{k + 1}$
and there exists no normal subgroup $G'$ of $G$ such that:
:$G_k \subset G' \subset G_{k + 1}$.
Now consider the sequence $\SS$:
:$H = G_0 \subset G_1 \subset \dots \subset G_n = G$
We can construct a normal series $\GG_1$ for $G / H$ from $\SS$:
:$H = G_0 / H \subset G_1 / H \subset \dots \subset G_n / H = G / H$
$\GG_1$ is indeed a normal series for $G / H$ because:
:$G_k \vartriangleleft G_{k + 1}$ by construction
:$H \vartriangleleft G_k$
:$\paren {G_{k + 1} / H} / \paren {G_k / H} \cong G_{k + 1} / G_k$ by Third Isomorphism Theorem.
{{AimForCont}} there exists a normal subgroup $G' / H$ of $G / H$ such that:
:$G_k / H \subset G' / H \subset G_{k + 1} / H$ 
for $k = 0, \dots, n - 1$.
Then the Third Isomorphism Theorem implies:
:$\paren {G' / H} / \paren {G_k / H} \cong G' / G_k$
Then $G_k$ is a proper normal subgroup of $G'$, contradicting the construction of $\GG$.
So no such $G' / H$ exists.
Hence, $\GG_1$ has no proper refinements and is a composition series.
Since the isomorphism $\paren {G_{k + 1} / H} / \paren {G_k / H} \cong G_{k + 1} / G_k$ holds for all $G_k, G_{k + 1}$:
:the length of $\SS$ is equal to $\map l {\GG_1} = \map l {G / H}$.
The result follows from the construction of $\GG$.
{{qed}}
Theorem: Condition for Composition Series

Let $G$ be a finite group.
Then:
:a normal series $\HH$ for $G$ is a composition series for $G$
{{iff}}:
:every factor group of $\HH$ is a simple group.

Proof:
Let $G$ be a finite group whose identity is $e$.
Let:
:$(1): \quad \set e = G_0 \lhd G_1 \lhd \cdots \lhd G_{n - 1} \lhd G_n = G$
be a normal series for $G$.