nyuuzyou/wikis huggingface dataset:
Equality of Ordered Pairs/Necessary Condition/Proof from Kuratowski Formalization

== Theorem ==
== Proof ==
First a lemma:
Let $\tuple {a, b} = \tuple {c, d}$.
From the Kuratowski formalization:
:$\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} }$ 
There are two cases: either $a = b$, or $a \ne b$.
==== Case 1 ====
Suppose $a = b$.
Then:
:$\set {\set a, \set {a, b} } = \set {\set a, \set a} = \set {\set a}$
Thus $\set {\set c, \set {c, d} }$ has only one element.
Thus $\set c = \set {c, d}$ and so $c = d$.
So:
:$\set {\set c, \set {c, d} } = \set {\set a}$
and so $a = c$ and $b = d$.
Thus the result holds.
==== Case 2 ====
Now suppose $a \ne b$. By the same argument it follows that $c \ne d$.
So that means that either $\set a = \set c$ or $\set a = \set {c, d}$.
Since $\set {c, d}$ has $2$ distinct elements, $\set a \ne \set {c, d}$.
Thus:
:$\set a = \set c$
and so $a = c$.
Then:
:$\set {a, b} = \set {c, d}$
But as $a = c$ that means we have:
:$\set {a, b} = \set {a, d}$
It follows from the lemma that:
:$b = d$
== Sources ==
* : $\S 6$: Ordered Pairs
* : Exercise $1.1: \ 12$
* : Chapter $\text I$: Algebraic Structures: $\S 1$: The Language of Set Theory: Exercise $1.11$
* : $\S 3$. Ordered pairs; cartesian product sets: Theorem $3.1$
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions
* : $1$. Notation, Conventions: $9$: Theorem $1.3$
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Theorem $4.4$.
Category:Equality of Ordered Pairs
Equality of Ordered Pairs/Necessary Condition/Proof from Wiener Formalization

== Theorem ==
== Proof ==
First a lemma:
Let $\tuple {a, b} = \tuple {c, d}$.
From the Wiener formalization:
:$\set {\set {\O, \set a}, \set {\set b} } = \set {\set {\O, \set c}, \set {\set d} }$
Let $x \in \set {\set {\O, \set a}, \set {\set b} }$.
Then either:
:$x = \set {\O, \set a}$
or:
:$x = \set {\set b}$
First suppose $x = \set {\O, \set a}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
 $x = \set {\set d}$.
That is:
:$\set {\O, \set a} = \set {\set d}$
Then:
:$\set d = \set a$
and also:
:$\set d = \O$
But that means:
:$a \in \O$
which contradicts the definition of the empty set $\O$.
It follows by Proof by Contradiction that $x \ne \set {\set d}$.
Thus $x = \set {\O, \set c}$.
We have that:
:$x = \set {\O, \set a}$ and $x = \set {\O, \set c}$
and so:
:$\set {\O, \set a} = \set {\O, \set c}$
It follows from the lemma that:
:$\set a = \set c$
Hence from Singleton Equality:
:$a = c$
Now suppose $x = \set {\set b}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
 $x = \set {\O, \set c}$.
That is:
:$\set {\set b} = \set {\O, \set c}$
which means that $\set b = \O$ and $\set b = \set c$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, \set c}$.
Thus $x = \set {\set d}$.
We have that:
:$x = \set {\set b}$ and $x = \set {\set d}$
By Singleton Equality:
:$\set b = \set d$
and again by Singleton Equality:
:$b = d$
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 4$ The pairing axiom: Exercise $4.1. \ \text{(b)}$
Category:Equality of Ordered Pairs
Equality of Ordered Pairs/Sufficient Condition

== Theorem ==
Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs.
Let $a = c$ and $b = d$.
Then:
:$\tuple {a, b} = \tuple {c, d}$
== Proof ==
Suppose $a = c$ and $b = d$.
Then:
:$\set a = \set c$
and:
:$\set {a, b} = \set {c, d}$
Thus:
:$\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} }$
and so by the Kuratowski formalization:
:$\tuple {a, b} = \tuple {c, d}$
== Sources ==
* : $\S 3$. Ordered pairs; cartesian product sets: Theorem $3.1$
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions
* : $1$. Notation, Conventions: $9$: Theorem $1.3$
Category:Equality of Ordered Pairs
Equality of Ordered Tuples

== Theorem ==
Let $a = \tuple {a_1, a_2, \ldots, a_n}$ and $b = \tuple {b_1, b_2, \ldots, b_n}$ be ordered tuples.
Then:
:$a = b \iff \forall i: 1 \le i \le n: a_i = b_i$
That is, for two ordered tuples to be equal, all the corresponding elements have to be equal.
== Proof ==
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\tuple {a_1, a_2, \ldots, a_n} = \tuple {b_1, b_2, \ldots, b_n} \iff \forall i: 1 \le i \le n: a_i = b_i$
$\map P 1$ is true, as this just says $\tuple {a_1} = \tuple {b_1} \iff a_1 = b_1$ which is trivial.
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\tuple {a_1, a_2} = \tuple {b_1, b_2} \iff a_1 = b_1, a_2 = b_2$
which has been proved in Equality of Ordered Pairs.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\tuple {a_1, a_2, \ldots, a_k} = \tuple {b_1, b_2, \ldots, b_k} \iff \forall i: 1 \le i \le n: a_i = b_i$
Then we need to show:
:$\tuple {a_1, a_2, \ldots, a_{k + 1} } = \tuple {b_1, b_2, \ldots, b_{k + 1} } \iff \forall i: 1 \le i \le n: a_i = b_i$
=== Induction Step ===
This is our induction step:
But from the induction hypothesis we have that:
:$\tuple {a_2, \ldots, a_{k + 1} } = \tuple {b_2, \ldots, b_{k + 1} } \iff \forall i: 1 \le 2 \le k + 1: a_i = b_i$
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \N_{>0}: \tuple {a_1, a_2, \ldots, a_n} = \tuple {b_1, b_2, \ldots, b_n} \iff \forall i: 1 \le i \le n: a_i = b_i$
== Examples ==
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 18$: Induced $N$-ary Operations
* : $\S 1.15$: Sequences
* : $\S 8$: Cartesian product of sets
* : $\S 1$: Naive Set Theory: $\S 1.4$: Sets of Sets
* : Appendix $\text{A}.10$: Finite Sequences
* : Chapter $1$: Pairing
Category:Cartesian Product
Category:Equality of Ordered Tuples
Category:Equality
Equality of Ordered Tuples/Examples/Ordered Triple

== Example of Equality of Ordered Tuples ==
Let:
:$\tuple {a_1, a_2, a_3}$ and $\tuple {b_1, b_2, b_3}$
be ordered triples.
Then:
:$\tuple {a_1, a_2, a_3} = \tuple {b_1, b_2, b_3}$
:
:$\forall i \in \set {1, 2, 3}: a_i = b_i$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 3$. Ordered pairs; cartesian product sets: Exercise $4$
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions: Exercise $5$
Category:Equality of Ordered Tuples
Category:Equality of Ordered Triples
Equality of Polynomials

== Definition ==
Let $\left({k, +, \circ}\right)$ be an infinite field.
Let $k \left[{\left\{ {X_j: j \in J}\right\} }\right]$ be the ring of polynomial forms in the indeterminates $\left\{ {X_j: j \in J}\right\}$.
Let $f, g \in k \left[{\left\{ {X_j: j \in J}\right\} }\right]$
Then $f$ and $g$ are:
* equal as functions if the polynomial functions associated to $f$ and $g$ are equal as functions, that is:
::$\forall x \in k^J: f \left({x}\right) = g \left({x}\right)$
where $k^J$ is the free module on $J$.
* equal as forms if the functions $M \to k$ from the free commutative monoid to $k$ which define $f$ and $g$ are equal as functions.
== Theorem ==
$f$ and $g$ are equal as polynomials $f$ and $g$ are equal as functions.
Thus we can say $f = g$ without ambiguity as to what it means.
== Proof ==
Category:Polynomial Theory
Equality of Radial Distance Function to Riemannian Distance

== Theorem ==
Let $\struct {M, g}$ be a connected Riemannian manifold.
Let $U_p = \map {\exp_p} {\map {B_\epsilon} 0 }$ be an open or closed geodesic ball around $p \in M$.
Let $r : U_p \to \R$ be the radial distance function.
Let $d_g$ be the Riemannian distance.
Then:
:$\forall p \in M : \forall x \in U_p : \map r x = \map {d_g} {p, x}$
== Proof ==
== Sources ==
* : $\S 6$: Geodesics and Distance. Geodesics Are Locally Minimizing
Category:Riemannian Manifolds
Equality of Rational Numbers

== Theorem ==
Let $a, b, c, d$ be integers, with $b$ and $d$ nonzero.
:$(1): \quad$ The rational numbers $\dfrac a b$ and $\dfrac c d$ are equal.
:$(2): \quad$ The integers $a d$ and $b c$ are equal.
== Proof ==
Note that by definition, $\Q$ is the field of quotients of $\Z$.
=== 1 implies 2 ===
Let $\dfrac a b = \dfrac c d$ in $\Q$.
Then $b c = a d$ in $\Q$.
By Canonical Mapping to Field of Quotients is Injective, $b c = a d$ in $\Z$.
=== 2 implies 1 ===
Let $bd = ac$ in $\Z$.
By definition of ring homomorphism, $b c = a d$ in $\Q$.
Thus Let $\dfrac a b = \dfrac c d$ in $\Q$.
== Sources ==
* : Introduction: Review of Algebra, Geometry, and Trigonometry: $\text{0-1}$: The Real Numbers
Category:Rational Numbers
Category:Equality
Equality of Ratios Ex Aequali

== Theorem ==
That is, if:
:$a : b = d : e$
:$b : c = e : f$
then:
:$a : c = d : f$
== Proof ==
Let there be any number of magnitudes $A, B, C$, and others $D, E, F$ equal to them in multitude, which taken two and two together are in the same ratio, so that:
:$A : B = D : E$
:$B : C = E : F$
Then we need to show that:
:$A : C = D : F$
:
Let equimultiples $G, H$ be taken of $A, D$.
Let other arbitrary equimultiples $K, L$ be taken of $B, E$.
Let other arbitrary equimultiples $M, N$ be taken of $C, F$.
We have that $A : B = D : E$.
So from Multiples of Terms in Equal Ratios $G : K = H : L$.
For the same reason, $K : M = L : N$.
We have that there are three magnitudes $G, K, M$ and others $H, L, N$ which taken two and two together are in the same ratio.
So from Relative Sizes of Successive Ratios it follows that:
:$G > M \implies H > N$
:$G = M \implies H = N$
:$G < M \implies H < N$
We also have that $G, H$ are equimultiples of $A, D$ and that $M, N$ are equimultiples of $C, F$.
So from , $A : C = D : F$.
== Sources ==
* : Book $\text{V}$. Propositions
Category:Ratios
Equality of Ratios in Perturbed Proportion

== Theorem ==
That is, if:
:$a : b = e : f$
:$b : c = d : e$
then:
:$a : c = d : f$
== Proof ==
Let there be three magnitudes $A, B, C$, and others equal to them in multitude, which taken two and two together are in the same proportion, namely $D, E, F$.
Let the proportion of them be perturbed, that is:
:$A : B = E : F$
:$B : C = D : E$
then we need to show that:
:$A : C = D : F$
:
Let equimultiples $A, B, D$ be taken of $G, H, K$.
Let other arbitrary equimultiples $L, M, N$ be taken of $C, E, F$.
From Ratio Equals its Multiples it follows that $A : B = G : H$
For the same reason $E : F = M : N$.
We have that $A : B = E : F$
From Equality of Ratios is Transitive $G : H = M : N$.
Next, we have that $B : C = D : E$.
From Proportional Magnitudes are Proportional Alternately $B : D = C : E$.
From Ratio Equals its Multiples $B : D = H : K$.
We also have that $B : D = C : E$ and $H : K = C : E$.
So from Equality of Ratios is Transitive $H : K = C : E$.
From Ratio Equals its Multiples $C : E = L : M$.
We also have that $C : E = H : K$.
So from Equality of Ratios is Transitive $H : K = L : M$.
From Proportional Magnitudes are Proportional Alternately $H : L = K : M$.
But we have $G : H = M : N$.
Thus it follows from Relative Sizes of Elements in Perturbed Proportion that:
:$G > L \implies K > N$
:$G = L \implies K = N$
:$G < L \implies K < N$
We have that:
: $G, K$ are equimultiples of $A, D$
: $L, N$ are equimultiples of $C, F$
Therefore $A : C = D : F$.
== Sources ==
* : Book $\text{V}$. Propositions
Category:Ratios
Equality of Ratios is Transitive

== Theorem ==
That is:
:$A : B = C : D, C : D = E : F \implies A : B = E : F$
== Proof ==
Let $A : B = C : D$ and $C : D = E : F$.
:
Of $A, C, E$ let equimultiples $G, H, K$ be taken.
Of $B, D, F$ let other arbitrary equimultiples $L, M, N$ be taken.
We have that:
:$A : B = C : D$
:$G, H$ are equimultiples of $A, C$
:$L, M$ are equimultiples of $B, D$
So:
:$G > L \implies H > M$
:$G = L \implies H = M$
:$G < L \implies H < M$
Also, we have that:
:$C : D = E : F$
:$H, K$ are equimultiples of $C, E$
:$M, N$ are equimultiples of $D, F$
So:
:$H > M \implies K > N$
:$H = M \implies K = N$
:$H < M \implies K < N$
Also, we have that:
:$G, K$ are equimultiples of $A, E$
:$L, N$ are equimultiples of $B, F$
Therefore $A : B = E : F$.
== Sources ==
* : Book $\text{V}$. Propositions
Category:Ratios
Equality of Real Numbers/Examples/One Half

== Examples on Equality of Real Numbers ==
The numbers $\dfrac 1 2$ and $\dfrac 2 4$ are equal, as they both correspond with the point which is the midpoint of the line segment from $0$ to $1$ on the real number line.
== Sources ==
* : Introduction: Review of Algebra, Geometry, and Trigonometry: $\text{0-1}$: The Real Numbers
Category:Equality of Real Numbers
Equality of Relations

== Theorem ==
Let $\RR_1$ and $\RR_2$ be relations on $S_1 \times T_1$ and $S_2 \times T_2$ respectively.
Then $\RR_1$ and $\RR_2$ are equal :
:$S_1 = S_2$
:$T_1 = T_2$
:$\tuple {s, t} \in \RR_1 \iff \tuple {s, t} \in \RR_2$
It is worth labouring the point that for two relations to be equal, not only must their domains be equal, but so must their codomains.
== Proof ==
This follows from set equality and Equality of Ordered Pairs.
A relation on $S \times T$ is an ordered triple, thus:
From Equality of Ordered Tuples, $\RR_1 = \RR_1$ :
Then we have that $R_1$ and $R_2$ are sets of ordered pairs.
Thus by definition of set equality:
:$R_1 = R_2 \iff \paren {\forall \tuple {x, y} \in \S_1 \times T_2: \tuple {x, y} \in R_1 \iff \tuple {x, y} \in R_2}$
Hence the result.
== Also known as ==
Some sources refer to this concept between two relations as being equivalence, rather than equality.
== Sources ==
* : $\S 4$. Relations; functional relations; mappings
Category:Relation Theory
Category:Equality
Equality of Squares Modulo Integer is Equivalence Relation

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\RR_n$ be the relation on the set of integers $\Z$ defined as:
:$\forall x, y \in \Z: x \mathrel {\RR_n} y \iff x^2 \equiv y^2 \pmod n$
Then $\RR_n$ is an equivalence relation.
== Proof ==
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
We have that for all $x \in \Z$:
:$x^2 \equiv x^2 \pmod n$
It follows by definition of $\RR_n$ that:
:$x \mathrel {\RR_n} x$
Thus $\RR_n$ is seen to be reflexive.
=== Symmetry ===
Thus $\RR_n$ is seen to be symmetric.
=== Transitivity ===
Let:
:$x \mathrel {\RR_n} y$ and $y \mathrel {\RR_n} z$
for $x, y, z \in \Z$.
Then by definition:
Thus $\RR_n$ is seen to be transitive.
$\RR_n$ has been shown to be reflexive, symmetric and transitive.
Hence by definition it is an equivalence relation.
Category:Examples of Equivalence Relations
Equality of Successors implies Equality of Ordinals

== Theorem ==
Let $\On$ denote the class of all ordinals.
Then:
:$\forall \alpha, \beta \in \On: \alpha^+ = \beta^+ \implies \alpha = \beta$
== Proof ==
From Class of All Ordinals is Well-Ordered by Subset Relation:
:$\alpha^+$ is the immediate successor of $\alpha$
:$\beta^+$ is the immediate successor of $\beta$
and no two distinct elements of $\On$ can have the same immediate successor.
The result follows.
== Sources ==
* : Chapter $5$: Ordinal Numbers: $\S 1$ Ordinal numbers: Theorem $1.17$
Category:Ordinals
Equality of Terms of Natural Numbers is Provable

== Theorem ==
Let $A$ and $B$ be terms in the language of arithmetic containing no variables.
Let $A = B$ when interpreted over the natural numbers $\N$.
Then there is a formal proof of $A = B$ in minimal arithmetic.
== Proof ==
Let $k = A = B$.
By Unary Representation of Natural Number, there is a term $\sqbrk k$ consisting of only the successor mapping and the constant $0$ such that $\sqbrk k = k$.
We want to show that $A = \sqbrk k$ has a formal proof.
Proceed by induction on the structure of the term $A$.
By definition, a term consists of variables and function applications.
By assumption, $A$ contains no variables.
Therefore, $A$ consists of only function applications defined by the language.
=== Constant $0$ ===
Let $A = 0$.
Then the following is a formal proof:
:By Equality is Reflexive:
::$0 = 0$
=== Successor Mapping ===
Let $A' = \map s A$.
Then the following is a formal proof:
:By hypothesis, there is a formal proof of $A = \sqbrk k$.
:By Substitution Property of Equality:
::$\map s A = \map s {\sqbrk k}$
But $\map s {\sqbrk k}$ is syntactically identical to $\sqbrk {\map s k}$, and $\map s A$ to $A'$.
Therefore, there is a formal proof of $A' = \sqbrk {\map s k}$.
=== Addition ===
Let $A' = A_1 + A_2$
Then the following is a formal proof:
:By hypothesis, there are formal proofs of $A_1 = \sqbrk {k_1}$ and $A_2 = \sqbrk {k_2}$.
:By Addition of Natural Numbers is Provable, there is a formal proof of $\sqbrk {k_1} + \sqbrk {k_2} = \sqbrk {k_1 + k_2}$.
:By Substitution Property of Equality:
::$A_1 + A_2 = \sqbrk {k_1 + k_2}$
But as $A_1 = k_1$ and $A_2 = k_2$, it follows that $k_1 + k_2 = A_1 + A_2$.
Therefore, the formal proof above is syntactically identical to:
:$A' = \sqbrk {A_1 + A_2}$
=== Multiplication ===
Let $A' = A_1 \times A_2$
Then the following is a formal proof:
:By hypothesis, there are formal proofs of $A_1 = \sqbrk {k_1}$ and $A_2 = \sqbrk {k_2}$.
:By Multiplication of Natural Numbers is Provable, there is a formal proof of $\sqbrk {k_1} \times \sqbrk {k_2} = \sqbrk {k_1 \times k_2}$.
:By Substitution Property of Equality:
::$A_1 \times A_2 = \sqbrk {k_1 \times k_2}$
But as $A_1 = k_1$ and $A_2 = k_2$, it follows that $k_1 \times k_2 = A_1 \times A_2$.
Therefore, the formal proof above is syntactically identical to:
:$A' = \sqbrk {A_1 \times A_2}$
Thus, $A = \sqbrk k$ has a formal proof.
In exactly the same manner, $B = \sqbrk k$ has a formal proof.
But then the following is a formal proof:
:By Equality is Symmetric, $\sqbrk k = B$.
:By Equality is Transitive, $A = B$.
Category:Natural Numbers
Equality of Towers in Set

== Theorem ==
Let $X$ be a non-empty set.
Let $\struct {T_1, \preccurlyeq_1}$ and $\struct {T_2, \preccurlyeq_2}$ be towers in $X$.
Then either:
:$\struct {T_1, \preccurlyeq_1} = \struct {T_2, \preccurlyeq_2}$
or:
:$\struct {T_1, \preccurlyeq_1}$ is an initial segment of $\struct {T_2, \preccurlyeq_2}$ 
or:
:$\struct {T_2, \preccurlyeq_2}$ is an initial segment of $\struct {T_1, \preccurlyeq_1}$ 
== Proof ==
By the definition of tower:
:$\struct {T_1, \preccurlyeq_1}$ and $\struct {T_2, \preccurlyeq_2}$ are well-ordered sets.
By Wosets are Isomorphic to Each Other or Initial Segments, either:
:$(1): \quad$ the towers are order isomorphic to each other
or:
:$(2): \quad$ one is order isomorphic to an initial segment in the other.
, in case $(2)$, assume that $\struct {T_1, \preccurlyeq_1}$ is order isomorphic to an initial segment in $\struct {T_2, \preccurlyeq_2}$.
By Order Isomorphism iff Strictly Increasing Surjection, there exists a strictly increasing mapping:
:$i: \struct {T_1, \preccurlyeq_1} \to \struct {T_2, \preccurlyeq_2}$
such that $i \sqbrk {T_1}$, the image set of $T_1$ under $i$, is equal to $T_2$ or to an initial segment of $T_2$.
From Characterization of Strictly Increasing Mapping on Woset, we can characterize $i$ as follows:
:$\forall t \in T_1: \map i t = \map \min {T_2 \setminus i \sqbrk {S_t} }$
and:
:$i \sqbrk {S_t} = S_{\map i t}$
Define:
:$Y = \set {y \in T_1: \map i y = y}$
Then for any $t \in T_1$ and $S_t \subseteq Y$:
So $\map i y = y$ for any initial segment $S_t \subseteq Y$.
By Induction on Well-Ordered Set, $Y = T$.
Thus $i$ is the identity mapping from $T_1$ onto its image.
Recall that the image set of $i$ is $T_2$ or an initial segment of $T_2$.
So $T_1 = T_2$ or an initial segment of $T_2$.
== Sources ==
* $\S 1.11$ Supplementary Exercise $7$
Category:Well-Orderings
Equality of Vector Quantities

== Theorem ==
Two vector quantities are equal they have the same magnitude and direction.
That is:
:$\mathbf a = \mathbf b \iff \paren {\size {\mathbf a} = \size {\mathbf b} \land \hat {\mathbf a} = \hat {\mathbf b} }$
where:
:$\hat {\mathbf a}$ denotes the unit vector in the direction of $\mathbf a$
:$\size {\mathbf a}$ denotes the magnitude of $\mathbf a$.
== Proof ==
Let $\mathbf a$ and $\mathbf b$ be expressed in component form:
where $\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n$ denote the unit vectors in the positive directions of the coordinate axes of the Cartesian coordinate space into which $\mathbf a$ has been embedded.
Thus $\mathbf a$ and $\mathbf b$ can be expressed as:
By definition of vector length, we have that:
and similarly:
From Vector Quantity as Scalar Product of Unit Vector Quantity, it follows that:
and similarly:
=== Sufficient condition ===
Let $\mathbf a = \mathbf b$.
Then by Equality of Ordered Tuples:
:$(1): \quad a_1 = b_1, a_2 = b_2, \ldots a_n = b_n$
Then:
and:
=== Necessary Condition ===
Let $\size {\mathbf a} = \size {\mathbf b}$, and $\hat {\mathbf a} = \hat {\mathbf b}$.
Then:
== Sources ==
* : Chapter $\text I$. Addition and Subtraction of Vectors. Centroids: Definitions: $3$. Definitions of terms
* : Chapter $\text I$: Definitions. Elements of Vector Algebra: $2$. Graphical Representation of Vectors
* : $\S 1$: $n$-Dimensional vector spaces
* : Chapter $\text {V}$: Vector Spaces: $\S 26$. Vector Spaces and Modules
* : $\S 22$: Fundamental Definitions: $1.$
* 
* 
* : $\S 20$: Formulas from Vector Analysis: Fundamental Definitions: $1.$
Category:Vectors
Category:Equality
Equality to Initial Segment Imposes Well-Ordering

== Theorem ==
Let $X$ be a set.
Let $\AA$ be the set of all ordered pairs $\struct {A, <}$ such that $A$ is a subset of $X$ and $<$ is a strict well-ordering of $A$.
Define $\prec$ as:
:$\struct {A, <} \prec \struct {A', <'}$
 
:$\struct {A, <}$ equals an initial segment of $\struct {A', <'}$.
Let $\BB$ be a set of ordered pairs in $\AA$ such that $\BB$ is ordered by $\prec$.
Let $B'$ be the union of the sets $B$ for all $\struct {B, <} \in \BB$.
Let $<'$ be the union of the relations $<$ for all $\struct {B, <}$.
Then $\struct {B', <'}$ is strictly well-ordered set.
== Proof ==
If the set $X$ considered is empty or a singleton, the lemma holds vacuously or trivially.
Thus assume $X$ contains at least two elements.
We first prove that $\prec$ is a strict partial ordering on $\AA$.
From the definition of initial segment, no $\struct {A, <}$ can equal an initial segment of itself.
Thus $\prec$ is antireflexive.
Suppose $\struct {A, <_A}$ equals an initial segment of $\struct {B, <_B}$ and $\struct {B, <_B}$ equals an initial segment of $\struct {C, <_C}$.
Then $\struct {A, <_A}$ equals an initial segment of $\struct {C, <'}$ from Equality is Transitive.
Thus $\prec$ is a strict partial ordering on $\AA$.
We then prove that any $\struct {B', <'}$ is a strictly well-ordered set.
Let $x_1,x_2 \in B'$.
That is, let $x_i \in \struct {A_i, <_i}$ for $i = 1, 2$.
Suppose $x_2 \prec x_1$.
That is, $\struct {A_2, <_2}$ equals an initial segment in $\struct {A_1, <_1}$
By the definition of initial segment, both $x_1$ and $x_2$ are in $\struct {A_1, <_1}$.
Thus $<'$ is connected, as all $<_i$ are strict well-orderings by hypothesis.
For any $x_i \in \struct {A_i, <_i}$, $x_i \nprec x_i$ as all $<_i$ are strict well-orderings by hypothesis.
Thus $<'$ is antireflexive.
To show that $<'$ is transitive, consider $x_i \in \struct {B', <'}$ for $i = 1, 2, 3$.
Suppose $x_1 <' x_2 <' x_3$.
Then $x_1 <_1 x_2$ and $x_2 <_2 x_3$, from the definition of $<'$ as a union of relations $<_i$.
Then $\struct {A_j, <_j}$ is an initial segment of $\struct {A_i, <_i}$ for $j = 1, 2; j < i$
Thus $x_1 <_i x_2 <_i x_3$.
Then $x_1 <_i x_3$, as all $<_i$ as all $<_i$ are strict well-orderings by hypothesis.
Conclude that $<'$ is itself a strict ordering.
It remains to be shown that $<'$ is a well-ordering.
Let $A$ be an arbitrary non-empty subset of $B'$.
Let $x \in A$ and $x \in \struct {B, <}$ for $\struct {B, <} \in \BB$.
Then for all $y \in A$, $y <' x$ $y < x$ and $y \in B$.
As $<$ is a well-ordering, $\struct {B \cap A, <}$ has a smallest element $b$.
This $b$ is then a smallest element of $<'$ in $A$.
Conclude that $<'$ is a strict well-ordering on $B'$.
== Sources ==
* : Supplementary Exercises $1.5$
Category:Well-Orderings
Category:Set Equality