avewright/proofwiki-math huggingface dataset:
Theorem: Composition of Ring Homomorphisms is Ring Homomorphism

Let:
:$\struct {R_1, +_1, \odot_1}$
:$\struct {R_2, +_2, \odot_2}$
:$\struct {R_3, +_3, \odot_3}$
be rings.
Let:
:$\phi: \struct {R_1, +_1, \odot_1} \to \struct {R_2, +_2, \odot_2}$
:$\psi: \struct {R_2, +_2, \odot_2} \to \struct {R_3, +_3, \odot_3}$
be homomorphisms.
Then the composite of $\phi$ and $\psi$ is also a homomorphism.

Proof:
Let $\psi \circ \phi$ denote the composite of $\phi$ and $\psi$.
Then what we are trying to prove is denoted:
:$\paren {\psi \circ \phi}: \struct {R_1, +_1, \odot_1} \to \struct {R_3, +_3, \odot_3}$ is a homomorphism.
To prove the above is the case, we need to demonstrate that the morphism property is held by $+_1$ and $\odot_1$ under $\psi \circ \phi$.
We take two elements $x, y \in R_1$, and put them through the following wringer with respect to $+_1$:
{{begin-eqn}}
{{eqn | l = \map {\paren {\psi \circ \phi} } {x +_1 y}
      | r = \map \psi {\map \phi {x +_1 y} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \psi {\map \phi x +_2 \map \phi y}
      | c = Morphism Property applied to $+_1$ under $\phi$
}}
{{eqn | r = \map \psi {\map \phi x} +_3 \map \psi {\map \phi y}
      | c = Morphism Property applied to $+_2$ under $\psi$
}}
{{eqn | r = \map {\paren {\psi \circ \phi} } x +_3 \map {\paren {\psi \circ \phi} } y
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
The same applies to $\odot_1$:
{{begin-eqn}}
{{eqn | l = \map {\paren {\psi \circ \phi} } {x \odot_1 y}
      | r = \map \psi {\map \phi {x \odot_1 y} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \psi {\map \phi x \odot_2 \map \phi y}
      | c = Morphism Property applied to $\odot_1$ under $\phi$
}}
{{eqn | r = \map \psi {\map \phi x} \odot_3 \map \psi {\map \phi y}
      | c = Morphism Property applied to $\odot_2$ under $\psi$
}}
{{eqn | r = \map {\paren {\psi \circ \phi} } x \odot_3 \map {\paren {\psi \circ \phi} } y
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
Disentangling the confusing and tortuous expressions above, we (eventually) see that this shows that the morphism property is indeed held by both $+_1$ and $\circ_1$ under $\psi \circ \phi$.
Thus $\paren {\psi \circ \phi}: \struct {R_1, +_1, \odot_1} \to \struct {R_3, +_3, \odot_3}$ is a homomorphism.
{{qed}}
Theorem: Composition of Ring Epimorphisms is Ring Epimorphism

Let:
:$\struct {R_1, +_1, \circ_1}$
:$\struct {R_2, +_2, \circ_2}$
:$\struct {R_3, +_3, \circ_3}$
be rings.
Let:
:$\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$
:$\psi: \struct {R_2, +_2, \circ_2} \to \struct {R_3, +_3, \circ_3}$
be (ring) epimorphisms.
Then the composite of $\phi$ and $\psi$ is also a (ring) epimorphism.

Proof:
A ring epimorphism is a ring homomorphism which is also a surection.
From Composition of Ring Homomorphisms is Ring Homomorphism, $\psi \circ \phi$ is a ring homomorphism.
From Composite of Surjections is Surjection, $\psi \circ \phi$ is a surection.
{{qed}}
Theorem: Composition of Ring Monomorphisms is Ring Monomorphism

Let:
:$\struct {R_1, +_1, \circ_1}$
:$\struct {R_2, +_2, \circ_2}$
:$\struct {R_3, +_3, \circ_3}$
be rings.
Let:
:$\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$
:$\psi: \struct {R_2, +_2, \circ_2} \to \struct {R_3, +_3, \circ_3}$
be (ring) monomorphisms.
Then the composite of $\phi$ and $\psi$ is also a (ring) monomorphism.

Proof:
A ring monomorphism is a ring homomorphism which is also an injection.
From Composition of Ring Homomorphisms is Ring Homomorphism, $\psi \circ \phi$ is a ring homomorphism.
From Composite of Injections is Injection, $\psi \circ \phi$ is an injection.
{{qed}}
Theorem: Composition of Ring Isomorphisms is Ring Isomorphism

Let:
* $\left({R_1, +_1, \circ_1}\right)$
* $\left({R_2, +_2, \circ_2}\right)$
* $\left({R_3, +_3, \circ_3}\right)$
be rings.
Let:
* $\phi: \left({R_1, +_1, \circ_1}\right) \to \left({R_2, +_2, \circ_2}\right)$
* $\psi: \left({R_2, +_2, \circ_2}\right) \to \left({R_3, +_3, \circ_3}\right)$
be (ring) isomorphisms.
Then the composite of $\phi$ and $\psi$ is also a (ring) isomorphism.

Proof:
A ring isomorphism is a ring homomorphism which is also a bijection.
From Composition of Ring Homomorphisms is Ring Homomorphism, $\psi \circ \phi$ is a ring homomorphism.
From Composite of Bijections is Bijection, $\psi \circ \phi$ is a bijection.
{{qed}}
Theorem: Composition of Ring Endomorphisms is Ring Endomorphism

Let $R$ be a set.
Let:
: $\struct {R, +_1, \circ_1}$
: $\struct {R, +_2, \circ_2}$
: $\struct {R, +_3, \circ_3}$
be rings.
Let:
: $\phi: \struct {R, +_1, \circ_1} \to \struct {R, +_2, \circ_2}$
: $\psi: \struct {R, +_2, \circ_2} \to \struct {R, +_3, \circ_3}$
be (ring) endomorphisms.
{{Questionable|They are between different rings, just with the same underlying set. Are they endomorphisms?}}
Then the composite of $\phi$ and $\psi$ is also a (ring) endomorphism.

Proof:
A ring endomorphism is a ring homomorphism $f$ from a set to itself.
That is:
:$\Dom \phi = \Cdm \phi$
:$\Dom \psi = \Cdm \psi$
From Composition of Ring Homomorphisms is Ring Homomorphism, $\psi \circ \phi$ is a ring homomorphism.
By definition of composition of mappings:
:$\Cdm \phi = \Dom \psi$
Thus:
:$\Dom \phi = \Cdm \psi = R$
and so $\psi \circ \phi$ is a ring endomorphism.
{{qed}}
Theorem: Composition of Ring Automorphisms is Ring Automorphism

Let $R$ be a set.
Let:
* $\struct {R, +_1, \circ_1}$
* $\struct {R, +_2, \circ_2}$
* $\struct {R, +_3, \circ_3}$
be rings.
Let:
* $\phi: \struct {R, +_1, \circ_1} \to \struct {R, +_2, \circ_2}$
* $\psi: \struct {R, +_2, \circ_2} \to \struct {R, +_3, \circ_3}$
be ring automorphisms.
{{Questionable|They are between different rings, just with the same underlying set. Are they automorphisms?}}
Then the composite of $\phi$ and $\psi$ is also a (ring) automorphism.

Proof:
A ring automorphism is a ring isomorphism $f$ from a set to itself.
That is:
:$\Dom \phi = \Cdm \phi$
:$\Dom \psi = \Cdm \psi$
From Composition of Ring Isomorphisms is Ring Isomorphism, $\psi \circ \phi$ is a ring isomorphism.
By definition of composition of mappings:
:$\Cdm \phi = \Dom \psi$
Thus:
:$\Dom \phi = \Cdm \psi = R$
and so $\psi \circ \phi$ is a ring automorphism.
{{qed}}
Theorem: Set has Rank

Let $S$ be a set.
Then $S$ has a rank.

Proof:
The proof shall proceed by Epsilon Induction on $S$.
Suppose that all the elements $a \in S$ have a rank.
That is, $a \in \map V x$ for some $x$.
Let:
:$\ds \map F a = \inf \set {x \in \On : a \in \map V x}$
be the rank of $a$.
Let:
:$\ds y = \sup \set {\map F a : a \in S}$
be the least level of the Von Neumann Hierarchy containing all elements of $S$.
Then, for any $a \in S$:
{{begin-eqn}}
{{eqn | l = a
      | o = \in
      | r = \map V {\map F a}
      | c = Definition of $F$
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \in
      | r = \map V y
      | c = Definition of $y$
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = \map V y
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \in
      | r = \powerset {\map V y}
      | c = {{Defof|Power Set}}
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \in
      | r = \map V {y + 1}
      | c = {{Defof|Von Neumann Hierarchy}}
}}
{{end-eqn}}
Therefore $S \in \map V z$ for some ordinal $z = y + 1$.
Thus by Epsilon Induction every set has a rank.
{{qed}}
Theorem: Quotient Epimorphism is Epimorphism/Group

Let $G$ be a group.
Let $N$ be a normal subgroup of $G$.
Let $G / N$ be the quotient group of $G$ by $N$.
Let $q_N: G \to G / N$ be the quotient epimorphism from $G$ to $G / N$:
:$\forall x \in G: \map {q_N} x = x N$
Then $q_N$ is a group epimorphism whose kernel is $N$.

Proof:
The proof follows from Quotient Mapping on Structure is Epimorphism.
When $N \lhd G$, we have:
{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = \map {q_N} {x y}
      | r = x y N
      | c = {{Defof|Quotient Group Epimorphism}}
}}
{{eqn | r = \paren {x N} \paren {y N}
      | c = {{Defof|Quotient Group}}
}}
{{eqn | r = \map {q_N} x \map {q_N} y
      | c = {{Defof|Quotient Group Epimorphism}}
}}
{{end-eqn}}
Therefore $q$ is a homomorphism.
We have that:
:$\forall x \in G: x N \in G / N = \map {q_N} x$
so $q$ is surjective.
Therefore $q$ is an epimorphism.
Let $x \in G$.
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map \ker {q_N}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {q_N} x
      | r = e_{G/N}
      | c = {{Defof|Kernel of Group Homomorphism}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x N
      | r = e_{G/N} N
      | c = {{Defof|Quotient Group Epimorphism}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x N
      | r = N
      | c = Coset by Identity
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = N
      | c = Left Coset Equals Subgroup iff Element in Subgroup
}}
{{end-eqn}}
thus proving that $\map \ker {q_N} = N$ from definition of subset.
{{qed}}
Theorem: Strictly Increasing Mapping on Well-Ordered Class

Let $\struct {S, \prec}$ be a strictly well-ordered class.
Let $\struct {T, <}$ be a strictly ordered class.
Let $f$ be a mapping from $S$ to $T$.
For each $i \in S$ such that $i$ is not maximal in $S$, let:
: $\map f i < \map f {\map \Succ i}$
where $\map \Succ i$ is the immediate successor element of $i$.
Let:
:$\forall i, j \in S: i \preceq j \implies \map f i \le \map f j$
Then for each $i, j \in S$ such that $i \prec j$:
:$\map f i < \map f j$
{{MissingLinks|In the above, link to definitions of increasing mapping and strictly increasing mapping, in order to correlate with page title.}}

Proof:
{{NotZFC}}
By Non-Greatest Element of Well-Ordered Class has Immediate Successor, $\map \Succ i$ is guaranteed to exist.
Let $i \prec j$.
Let $S_i := \set {q \in S: i \prec q}$.
{{explain|Important to specify what the domain of $q$ actually is -- presumably $S$.}}
Then $\map \Succ i$ is the minimal element of $S_i$.
By supposition, $j \in S_i$.
Thus:
:$j \nprec \map \Succ i$
Since Well-Ordering is Total Ordering:
:$\map \Succ i \preceq j$
Thus by supposition:
:$\map f {\map \Succ i} \le \map f j$
Since $\map f i < \map f {\map \Succ i}$:
:$\map f i < \map f j$
by transitivity.
{{qed}}
Category:Class Mappings
Category:Increasing Mappings
358svmg7n2px81ky95a26i24nk81mso
Theorem: Non-Greatest Element of Well-Ordered Class has Immediate Successor

Let $C$ be a well-ordered class under an ordering $\le$.
Let $x \in C$.
Suppose that $x$ is not the greatest element in $C$.
Then $x$ has an immediate successor element in $C$.

Proof:
Let $x$ be an element of $C$ which is not the greatest element of $C$.
Let $S$ be the class of successor elements of $x$ in $C$.
We have that $S$ is a subclass of $C$.
Also, $S$ is non-empty because $x$ is not the greatest element.
Thus $S$ is a non-empty subclass of $C$.
We have {{hypothesis}} that $\le$ is a well-ordering on $C$
Hence $S$ has a smallest element, $y$.
By the definition of $S$:
:$x < y$ 
{{AimForCont}} that for some $z \in C$, $x < z < y$.
Then by the definition of $S$, $z \in S$.
This contradicts the fact that $y$ is the smallest element of $S$.
Thus $y$ is the immediate successor element of $x$.
{{qed}}
Theorem: Set Contained in Smallest Transitive Set

Let $S$ be a set.
Then there exists a transitive set $G$ such that:
:$S \subseteq G$
and:
:if $Q$ is any transitive set such that $S \subseteq Q$, then $G \subseteq Q$.

Proof:
=== Construction of $G$ ===
Let $U$ be the class of all sets.
{{explain|Perhaps Universal Class can be used here}}
Define the mapping $F: \N \to U$ recursively:
:$\map F 0 = S$
:$\map F {n + 1} = \bigcup \map F n$
Applying the axiom of union inductively, $\map F n$ is a set for each $n \in \N$.
Let $\ds G = \bigcup_{i \mathop = 0}^\infty \map F i$.
By the {{Axiom-link|Unions|Set Theory}}, $G$ is a set.
Theorem: Transitive Set Contained in Von Neumann Hierarchy Level

Let $G$ be a transitive set.
Then for some ordinal $i$, $G \subseteq V_i$.

Proof:
{{NotZFC}}
{{AimForCont}} for each ordinal $i$ the set $G \setminus V_i$ is non-empty. 
Let $i$ be any ordinal.
Then by the axiom of foundation:
$\exists x: x \in G\setminus V_i \text{ and } x \cap \paren {G \setminus V_i} = \O$
Since $G$ is transitive, $x \subseteq G$.
Since $x \subseteq G$ and $x \cap \paren {G \setminus V_i} = \O$:
:$x \subseteq V_i$
By the definition of $V$, $x \in V_{i + 1}$, so:
:$x \notin G \setminus V_{i + 1}$
Thus $G \setminus V_{i + 1} \subsetneqq G \setminus V_i$ for each ordinal $i$.
Let $H: \On \to \powerset G$ be defined by:
:$\map H i = G \setminus V_i$ for each ordinal $i$
Since the class of ordinals is well-ordered, applying Strictly Increasing Mapping on Well-Ordered Class proves that for any ordinals $p$ and $q$,
:$p < q$ implies $\map H q \subsetneq \map H p$.
Since the class of ordinals is totally ordered, for any two distinct ordinals $i$ and $j$:
: $\map H i \ne \map H j$
so $H$ is injective.
But that contradicts the fact that $\powerset G$ is a set.
{{qed}}
Category:Von Neumann Hierarchy
f3h22a244wn74sfo34k8tzq4iur0zd5
Theorem: External Direct Product Closure/General Result

Let $\ds \struct {S, \circ} = \prod_{k \mathop = 1}^n S_k$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$.
Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$ all be closed algebraic structures.
Then $\struct {S, \circ}$ is also a closed algebraic structure.

Proof:
Follows directly from External Direct Product Closure.
{{finish|Fill in the detail.}}
{{qed}}
Category:External Direct Product Closure
b3e434rvo0yrek6paldbzanjz0tu3f3
Theorem: External Direct Product of Abelian Groups is Abelian Group/General Result

The external direct product of a finite sequence of abelian groups is itself an abelian group.

Proof:
Let $\struct {G_1, \circ_1}, \struct {G_2, \circ_2}, \ldots, \struct {G_n, \circ_n}$ be abelian groups.
Let $\ds \struct {G, \circ} = \prod_{k \mathop = 1}^n G_k$ be the external direct product of $\struct {G_1, \circ_1}, \struct {G_2, \circ_2}, \ldots, \struct {G_n, \circ_n}$.
From External Direct Product of Groups is Group: Finite Product it follows that $\struct {G, \circ}$ is a group.
By definition, each of $\circ_1, \circ_2, \ldots, \circ_n$ are commutative operations.
From External Direct Product Commutativity: General Result it follows that $\circ$ is commutative.
Hence, by definition, $\struct {G, \circ}$ is an abelian group.
{{qed}}
Category:Abelian Groups
Category:Group Direct Products
2ws7diaaj30uoegpqbepqx8fb9k63y7
Theorem: Homomorphism of External Direct Products/General Result

Let $n \in \N_{>0}$.
Let:
{{begin-eqn}}
{{eqn | l = \struct {\SS_n, \circledcirc_n}
      | o = :=
      | m = \prod_{k \mathop = 1}^n S_k
      | mo= =
      | r = \struct {S_1, \circ_1} \times \struct {S_2, \circ_2} \times \cdots \times \struct {S_n, \circ_n}
}}
{{eqn | l = \struct {\TT_n, \circledast_n}
      | o = :=
      | m = \prod_{k \mathop = 1}^n T_k
      | mo= =
      | r = \struct {T_1, \ast_1} \times \struct {T_2, \ast_2} \times \cdots \times \struct {T_n, \ast_n}
}}
{{end-eqn}}
be external direct products of algebraic structures.
Let $\Phi_n: \struct {\SS_n, \circledcirc_n} \to \struct {\TT_n, \circledast_n}$ be the mapping defined as:
:$\Phi_n: \tuple {s_1, \ldots, s_n} := \begin{cases}
\map {\phi_1} {s_1} & : n = 1 \\
\tuple {\map {\phi_1} {s_1}, \map {\phi_2} {s_2} } & : n = 2 \\
\tuple {\map {\Phi_n} {s_1, \ldots, s_{n - 1} }, \map {\phi_n} {s_n} } & : n > 2 \\
\end{cases}$
That is:
:$\Phi_n: \tuple {s_1, \ldots, s_n} := \tuple {\map {\phi_1} {s_1}, \map {\phi_2} {s_2}, \ldots, \map {\phi_n} {s_n} }$
Let $\phi_k: \struct {S_k, \circ_k} \to \struct {T_k, \ast_k}$ be a homomorphism for each $k \in \set {1, 2, \ldots, n}$.
Then $\Phi_n$ is a homomorphism from $\struct {\SS_n, \circledcirc_n}$ to $\struct {\TT_n, \circledast_n}$.

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\Phi_n: \struct {\SS_n, \circledcirc_n} \to \struct {\TT_n, \circledast_n}$ is a homomorphism.
Theorem: Cesàro Mean

Let $\sequence {a_n}$ be a sequence of complex numbers.
Suppose that $\sequence {a_n}$ converges to $\ell$ in $\C$:
:$\ds \lim_{n \mathop \to \infty} a_n = \ell$
Then also:
:$\ds \lim_{n \mathop \to \infty} \frac {a_1 + \dotsb + a_n} n = \ell$

Proof:
For every fixed integer $n_0$, we write:
:$\ds \cmod {\frac {a_1 + \dotsb + a_n} n - \ell} \le \frac {\cmod {a_1 - \ell} + \dotsb + \cmod {a_n - \ell} } n \le \frac {n_0 \ds \sup_{k \mathop \le n_0} \cmod {a_k - \ell} } n + \sup_{n_0 \mathop < k \mathop \le n} \cmod {a_k - \ell}$
As $n$ tends to $+\infty$, we get:
:$\ds \limsup_{n \mathop \to \infty} \cmod {\frac {a_1 + \dotsb + a_n} n - \ell} \le \sup_{k \mathop > n_0} \cmod {a_k - \ell}$
As $n_0$ tends to $+\infty$, we finally conclude:
:$\ds \limsup_{n \mathop \to \infty} \cmod {\frac {a_1 + \dotsb + a_n} n - \ell} = 0$
{{qed}}
{{explain|More detailed justification and explanation of all the steps}}
Theorem: Characterization of Minimal Element

Let $C$ be a class.
Let $\prec$ be a relation on $C$.
Let $B$ be a subclass of $C$.
Let $x \in B$.
Let $S_x = \set {y \in C: y \prec x \text{ and } y \ne x}$ be the initial segment of $x$ in $C$.
Then $x$ is a minimal element of $B$ {{iff}} $B \cap S_x = \O$.

Proof:
=== Necessary Condition ===
Suppose $x$ is a minimal element of $B$.
Then for each $z \in B$ such that $z \ne x$, $z \nprec x$.
Thus $S_x \cap B = \O$.
{{qed|lemma}}
Theorem: Non-Empty Class has Element of Least Rank

Let $C$ be a class.
Let $C \ne \O$.
Then $C$ has an element of least rank.
That is:
:$\exists x \in C: \forall y \in C: \map {\operatorname {rank} } x \le \map {\operatorname {rank} } y$
where $\map {\operatorname {rank} } x$ is the rank of $x$.

Proof:
{{NotZFC}}
By Set has Rank, each element of $C$ has a rank.
Let $R$ be the class of ranks of elements of $C$.
$R$ is non-empty because $C$ is non-empty.
{{explain|This should follow from arbitrary intersections of ordinals being ordinals.}}
Since any non-empty class of ordinals has a least element, $R$ has a least element, $q$.
By the definition of $R$:
:$\exists x \in C: \map {\operatorname {rank} } x = q$
Then $x$ is an element of $C$ of least rank.
{{qed}}
Category:Von Neumann Hierarchy
tnnlggl2y8200831pulyn5x3h80ke97
Theorem: Reversed Contour is Contour

Let $\R^n$ be a real cartesian space of $n$ dimensions.
Let $C$ be a contour in $\R^n$ that is defined as a concatenation of a finite sequence $C_1, \ldots, C_n$ of directed smooth curves in $\R^n$.
Then the finite sequence of reversed directed smooth curves:
:$-C_n, -C_{n - 1}, \ldots, -C_1$
defines a contour that is independent of the parameterization of $C_1, \ldots, C_n$.

Proof:
Let $C_i$ be parameterized by the smooth path $\gamma_i: \closedint {a_i} {b_i} \to \C$ for all $i \in \set {1, \ldots, n}$.
From Reversed Directed Smooth Curve is Directed Smooth Curve, it follows that $-C_i$ is independent of the paraterization $\gamma_i$ of $C_i$.
We now prove that the end point of $-C_i$ is equal to the start point of $-C_{i - 1}$ for all $i \in \set {2, \ldots, n}$.
By definition of reversed directed smooth curve, $-C_i$ is parameterized by $\rho_i: \closedint {a_i} {b_i} \to \C$.
Here, $\map {\rho_i} t = \map {\gamma_i} {a_i + b_i - t}$.
From Reparameterization of Directed Smooth Curve Maps Endpoints To Endpoints, it follows that the endpoints $\map {\rho_i} {a_i}$ and $\map {\rho_i} {b_i}$ are independent of the parameterization $\rho_i$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\rho_i} {b_i}
      | r = \map {\phi_i} {a_i + b_i - b_i}
}}
{{eqn | r = \map {\phi_i} {a_i}
}}
{{eqn | r = \map {\phi_{i - 1} } {b_{i - 1} }
      | c = {{Defof|Contour (Complex Plane)}}
}}
{{eqn | r = \map {\rho_{i - 1} } {a_{i - 1} }
}}
{{end-eqn}}
By definition, it follows that $-C_n, \ldots, -C_1$ can be concatenated to form a contour.
{{qed}}
Theorem: Contour Integral along Reversed Contour

Let $C$ be a contour in the complex plane $\C$.
Let $f: \Img C \to \C$ be a continuous complex functions, where $\Img C$ denotes the image of $C$.
Then the contour integral of $f$ along the reversed contour $-C$ is:
:$\ds \int_{-C} \map f z \rd z = -\int_C \map f z \rd z$

Proof:
First, suppose that $C$ is a directed smooth curve in $\C$.
Let $C$ be parameterized by the smooth path $\gamma: \closedint a b \to \C$.
By definition of reversed directed smooth curve, $-C$ is parameterized by a smooth path $\rho: \closedint a b \to \C$ with $\rho = \gamma \circ \psi$.
Here, $\psi: \closedint a b \to \closedint a b$ is defined by $\map \psi t = a + b - t$.
From Derivatives of Function of $a x + b$:
:$\map {\psi'} t = -1$ for all $t \in \closedint a b$
Then:
{{begin-eqn}}
{{eqn | l = \int_C \map f z \rd z 
      | r = \int_a^b \map f {\map \rho t} \map {\rho'} t \rd t
      | c = {{Defof|Complex Contour Integral}}
}}
{{eqn | r = \int_a^b \map f {\map \gamma {\map \psi t} } \map {\gamma'} {\map \psi t} \map {\psi'} t \rd t
      | c = Derivative of Complex Composite Function
}}
{{eqn | r = -\int_a^b \map f {\map \gamma u} \map {\gamma'} u \rd u
      | c = substitution with $u = \map \psi t$, where $\map \psi a > \map \psi b$
}}
{{eqn | r = -\int_C \map f z \rd z
}}
{{end-eqn}}
{{qed|lemma}}
Next, suppose that $C$ is a contour.
Then $C$ is a concatenation of a finite sequence $C_1, \ldots, C_n$ of directed smooth curves.
By definition of reversed contour, $-C$ is a concatenation of the finite sequence $-C_n, \ldots, -C_1$ of directed smooth curves.
Then:
{{begin-eqn}}
{{eqn | l = \int_C \map f z \rd z 
      | r = \sum_{k \mathop = 1}^n \int_{-C_k} \map f z \rd z 
      | c = Contour Integral of Concatenation of Contours
}}
{{eqn | r = -\sum_{k \mathop = 1}^n \int_{C_k} \map f z \rd z 
      | c = from the result above, as each $C_k$ is a directed smooth curve
}}
{{eqn | r = -\int_C \map f z \rd z
}}
{{end-eqn}}
{{qed}}
Theorem: Strictly Well-Founded Relation determines Strictly Minimal Elements/Lemma

Let $A$ be a non-empty class.
Let $\RR$ be a strictly well-founded relation on $A$.
Then $A$ has a strictly minimal element under $\RR$.

Proof:
{{NotZFC}}
The general strategy of the proof is as follows:
We will recursively define a certain subset, $a$, of $A$.
We will use the fact that $\RR$ is a strictly well-founded relation to choose a strictly minimal element $m$ of $a$.
Then we will prove that $m$ is in fact a strictly minimal element of $A$.
For each $x \in A$, let $\map {\RR^{-1} } x$ denote the preimage under $\RR$ of $x$ in $A$.
For each class $C$, let $\map R C$ denote the set of elements of $C$ of minimal rank, and let $\map R \O = \O$.
That is:
For a given class $C$, let $\alpha_C$ be the smallest ordinal such that:
:$C \cap \map V {\alpha_C} \ne \O$
where $V$ is the von Neumann hierarchy.
Then let $\map R C$ denote the set $C \cap \map V {\alpha_C}$.
Let $F$ be a function defined recursively:
:$\map F 0 = \map R A$
:$\ds \map F {n + 1} = \bigcup_{y \mathop \in \map F n} \map R {\map {\RR^{-1} } y}$
{{refactor|Extract this lemma into its own page.|level = basic}}