nyuuzyou/wikis huggingface dataset:
Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Continuous Mapping

== Theorem ==
Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $\upsilon_i$ be the subspace topology of $Y_i$ relative to $\tau$. 
Let $p_i = \pr_i {\restriction_{Y_i}}$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is continuous.
== Proof ==
Let $V \in \tau_i$.
Let $\ds U = \prod_{i \mathop \in I} U_i$ where:
:$U_j = \begin{cases} X_j & j \ne i \\ V & j = i \end{cases}$
From Natural Basis of Product Topology, $U$ is an element of the the natural basis.
By definition of the product topology $\tau$ on the product space $\struct {X, \tau}$ the natural basis is a basis for the product topology.
It follows that:
:$U$ is open in $\struct {X, \tau}$
Let $x \in Y_i$.
Now:
By set equality:
:$\map {p_i^\gets} V = U \cap Y_i$
By definition of the subspace topology on $Y_i$:
:$\map {p_i^\gets} V \in \upsilon_i$
It follows that $p_i$ is continuous by definition.
Category:Subspace of Product Space is Homeomorphic to Factor Space
Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Injection

== Theorem ==
Let $\family {X_i}_{i \mathop \in I}$ be a family of sets where $I$ is an arbitrary index set.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the Cartesian product of $\family {X_i}_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $p_i = \pr_i {\restriction_{Y_i}}$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is an injection.
== Proof ==
Note that by definitions of a restriction and a projection then:
:$\forall y \in Y_i: \map {p_i} y = y_i$ 
Let $x, y \in Y_i$.
Then for all $j \in I \setminus \set i$:
:$x_j = z_j = y_j$
Let $\map {p_i} x = \map {p_i} y$.
Then:
:$x_i = y_i$
Thus:
:$x = y$
It follows that $p_i$ is an injection by definition.
Category:Subspace of Product Space is Homeomorphic to Factor Space
Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Lemma 1

== Theorem ==
Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
For all $k \in I$, let $\pr_k$ denote the projection from $X$ to $X_k$.
Let $z \in X$.
Let $i, k \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $p_i = \pr_i {\restriction_{Y_i} }$ be the restriction of $\pr_i$ to $Y_i$.
Let $V_k \in \tau_k$.
Let $\map {\pr_k^\gets } {V_k} \cap Y_i \ne \O$.
Then:
:$\map {p_i^\to} {\map {\pr_k^\gets} {V_k} \cap Y_i}$ is open in $\struct{X_i, \tau_i}$
== Proof ==
We have that $p_i$ is a bijection from the lemmas:
:$p_i$ is an injection 
:$p_i$ is a surjection 
Let $x \in X_i$.
Then:
By definition of $p_i$:
:$\map {p_i^{-1} } x = y$
where:
:$\forall j \in I : y_j = \begin {cases} z_j & j \ne i \\ x & j = i \end {cases}$
==== Case 1: $k = i$ ====
Let $k = i$.
Then:
So:
:$x \in \map {p_i} {\map {\pr_i^\gets} {V_i} \cap Y_i}$ $x \in V_i$
That is:
:$\map {p_i} {\map {\pr_i^\gets} {V_i} \cap Y_i} = V_i \in \tau_i$
==== Case 2: $k \ne i$ ====
Let $k \ne i$.
Then:
So:
:$x \in \map {p_i} {\map {\pr_i^\gets} {V_i} \cap Y_i}$ $z_k \in V_k$
Since $x \in X_i$ was arbitrary, then:
:$\map {p_i} {\map {\pr_i^\gets} {V_i} \cap Y_i} = X_i$ $z_k \in V_k$
Let $w \in \map {\pr_k^\gets} {V_k} \cap Y_i$ which is guaranteed since $\map {\pr_k^\gets} {V_k} \cap Y_i \ne \O$
By the definition of inverse image mapping then:
:$w_k = \map {\pr_k} w \in V_k$
By the definition of $Y_i$ then:
:$w_k = z_k$
So $z_k \in V_k$.
It follows that:
:$\map {p_i} {\map {\pr_i^\gets} {V_i} \cap Y_i} = X_i \in \tau_i$
In either case:
:$\map {p_i^\to} {\map {\pr_k^\gets} {V_k} \cap Y_i}$ is open in $\struct {X_i, \tau_i}$.
Category:Subspace of Product Space is Homeomorphic to Factor Space
Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Open Mapping

== Theorem ==
Let $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary index set.
Let $\ds \struct {X, \tau} = \prod_{i \mathop \in I} \struct {X_i, \tau_i}$ be the product space of $\family {\struct {X_i, \tau_i} }_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $\upsilon_i$ be the subspace topology of $Y_i$ relative to $\tau$. 
Let $p_i = \pr_i {\restriction_{Y_i} }$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is an open mapping.
== Proof ==
Let $U \in \upsilon_i$.
Let $x \in \map {p_i^\to} U$.
Then by definition of the direct image mapping:
:$\exists y \in U : x = \map {p_i} y$
By the definition of the subspace topology:
:$\exists U' \in \tau: U = U' \cap Y_i$
For all $k \in I$ let $\pr_k$ denote the projection from $X$ to $X_k$.
By definition of the natural basis of the product topology $\tau$:
:there exists a finite subset $J$ of $I$
and:
:for each $k \in J$, there exists a $V_k \in \tau_k$
such that:
:$\ds y \in \bigcap_{k \mathop \in J} \map {\pr_k^\gets} {V_k} \subseteq U'$
Then:
:$\ds y \in \paren {\bigcap_{k \mathop \in J} \map{\pr_k^\gets} {V_k} } \cap Y_i \subseteq U' \cap Y_i = U$
By definition of direct image mapping:
:$\ds x = \map {p_i} y \in \map {p_i^\to} {\paren {\bigcap_{k \mathop \in J} \map {\pr_k^\gets} {V_k} } \cap Y_i} \subseteq \map {p_i^\to} U$
Recall that $p_i$ is an injection.
Then:
Let $k \in J$.
==== Lemma ====
By :
:$\ds \bigcap_{k \mathop \in J} \map {p_i^\to} {\map{\pr_k^\gets} {V_k} \cap Y_i}$ is open in $\struct {X_i, \tau_i}$
Since $x \in \map {p_i^\to} U$ was arbitrary then it has been shown that:
:$\forall x \in \map {p_i^\to} U : \exists V \in \tau_i : x \in V \subseteq \map {p_i^\to} U$
Then by definition:
$\forall x \in \map {p_i^\to} U: \map {p_i^\to} U$ is a neighborhood of $x$.
From Set is Open iff Neighborhood of all its Points:
:$\map {p_i^\to} U$ is open in $\tau_i$.
Since $U \in \upsilon_i$ was arbitrary, $p_i$ is an open mapping.
Category:Subspace of Product Space is Homeomorphic to Factor Space
Subspace of Product Space is Homeomorphic to Factor Space/Proof 2/Surjection

== Theorem ==
Let $\family {X_i}_{i \mathop \in I}$ be a family of sets where $I$ is an arbitrary index set.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the Cartesian product of $\family {X_i}_{i \mathop \in I}$.
Let $z \in X$.
Let $i \in I$. 
Let $Y_i = \set {x \in X: \forall j \in I \setminus \set i: x_j = z_j}$.
Let $p_i = \pr_i {\restriction_{Y_i} }$, where $\pr_i$ is the projection from $X$ to $X_i$.
Then:
:$p_i$ is a surjection.
== Proof ==
Note that by definitions of a restriction and a projection then:
:$\forall y \in Y_i: \map {p_i} y = y_i$ 
Let $x \in X_i$.
Let $y \in Y_i$ be defined by:
:$\forall j \in I: y_j = \begin{cases}
z_j & j \ne i \\
x & j = i
\end{cases}$
Then:
:$\map {p_i} y = y_i = x$
It follows that $p_i$ is a surjection by definition.
Category:Subspace of Product Space is Homeomorphic to Factor Space
Subspace of Real Continuous Functions

== Theorem ==
Let $\mathbb J = \set {x \in \R: a \le x \le b}$ be a closed interval of the real number line $\R$.
Let $\map C {\mathbb J}$ be the set of all continuous real functions on $\mathbb J$.
Then $\struct {\map C {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Proof ==
By definition, $\map C {\mathbb J} \subseteq \R^{\mathbb J}$.
Let $f, g \in \map C {\mathbb J}$.
By Two-Step Vector Subspace Test, it needs to be shown that:
:$(1): \quad f + g \in \map C {\mathbb J}$
:$(2): \quad \lambda f \in \map C {\mathbb J}$ for any $\lambda \in \R$
$(1)$ follows by Sum Rule for Continuous Real Functions.
$(2)$ follows by Multiple Rule for Continuous Real Functions.
Hence $\struct {\map C {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.5$
Category:Vector Subspaces
Category:Analysis
Subspace of Real Differentiable Functions

== Theorem ==
Let $\mathbb J$ be an open interval of the real number line $\R$.
Let $\map \DD {\mathbb J}$ be the set of all differentiable real functions on $\mathbb J$.
Then $\struct {\map \DD {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Proof ==
Note that by definition, $\map \DD {\mathbb J} \subseteq \R^{\mathbb J}$. 
Let $f, g \in \map \DD {\mathbb J}$. 
Let $\lambda \in \R$.
From Linear Combination of Derivatives, we have that: 
:$f + \lambda g$ is differentiable on $\mathbb J$. 
That is: 
:$f + \lambda g \in \map \DD {\mathbb J}$
So, by One-Step Vector Subspace Test:
:$\struct {\map \DD {\mathbb J}, +, \times}_\R$ is a subspace of $\R^{\mathbb J}$. 
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.5$
Category:Vector Subspaces
Category:Differential Calculus
Subspace of Real Functions of Differentiability Class

== Theorem ==
Let $\mathbb J = \set {x \in \R: a < x < b}$ be an open interval of the real number line $\R$.
Let $\map {C^m} {\mathbb J}$ be the set of all continuous real functions on $\mathbb J$ in differentiability class $m$.
Then $\struct {\map {C^m} {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
=== Corollary ===
== Proof ==
Note that by definition, $\map {C^m} {\mathbb J} \subseteq \R^{\mathbb J}$.
Let $f, g \in \map {C^m} {\mathbb J}$.
Let $\lambda \in \R$.
Applying Linear Combination of Derivatives $m$ times we have: 
:$f + \lambda g$ is $m$-times differentiable on $\mathbb J$ with $m$th derivative $f^{\paren m} + \lambda g^{\paren m}$.
Since both $f$ and $g$ are of differentiability class $m$:
:$f^{\paren m}$ and $g^{\paren m}$ are continuous on $\mathbb J$. 
From Combined Sum Rule for Continuous Real Functions:
:$f^{\paren m} + \lambda g^{\paren m} = \paren {f + \lambda g}^{\paren m}$ is continuous on $\mathbb J$.
So:
:$f + \lambda g \in \map {C^m} {\mathbb J}$
Therefore, by One-Step Vector Subspace Test:
:$\struct {\map {C^m} {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.5$
Category:Vector Subspaces
Category:Analysis
Subspace of Riemann Integrable Functions

== Theorem ==
Let $\mathbb J = \set {x \in \R: a \le x \le b}$ be a closed interval of the real number line $\R$.
Let $\map \RR {\mathbb J}$ be the set of all Riemann integrable functions on $\mathbb J$.
Then $\struct {\map \RR {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Proof ==
Note that by definition, $\map \RR {\mathbb J} \subseteq \R^{\mathbb J}$. 
Let $f, g \in \map \RR {\mathbb J}$.
Let $\lambda \in \R$.
By Linear Combination of Definite Integrals:
:$f + \lambda g$ is Riemann integrable on $\mathbb J$.
That is: 
:$f + \lambda g \in \map \RR {\mathbb J}$
So by One-Step Vector Subspace Test:
:$\struct {\map \RR {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.5$
Category:Vector Subspaces
Category:Analysis
Subspace of Separable Metric Space is Separable

== Theorem ==
Let $\struct {X, d}$ be a separable metric space.
Let $\struct {Y, d_Y}$ be a metric subspace of $\struct {X, d}$.
Then $Y$ is separable.
== Proof ==
If $Y = X$, we are done immediately.
Now consider the case $Y \ne X$. 
Pick $x \in X \setminus Y$. 
Let $\set {x_n : n \in \N}$ be a countable everywhere dense subset of $X$.
Iterate over the pairs $\struct {n, k}$ where $n, k \in \N$. 
Check whether:
:$\map {B_{1/k} } {x_n} \cap Y \ne \O$
where $\map {B_{1/k} } {x_n}$ is the open ball of radius $r$, centered at $x_n$. 
If the intersection is non-empty, let $y_{n, k}$ be any element of $\map {B_{1/k} } {x_n} \cap Y$. 
Otherwise, let $y_{n, k} = x$.
Now consider the set $\mathcal S = \set {y_{n, k} : y_{n, k} \ne x}$.
Note that it is not yet known that $\mathcal S \ne \O$.
We show that $\mathcal S$. is everywhere dense.
Let $y \in Y$ and let $\epsilon > 0$ be arbitrary.
Let $k$ be such that $1/k < \epsilon/2$. 
Since $\set {x_n : n \in \N}$ is everywhere dense, there exists $x_n \in \set {x_n : n \in \N}$ such that: 
:$\ds \map d {y, x_n} < 1/k$
Now, we have that:
:$\map {B_{1/k} } {x_n} \cap Y \supseteq \set {y_{n, k} } \ne \O$
We are now assured that $\mathcal S \ne \O$. 
So, we have: 
So, from Condition for Point being in Closure, we have: 
:$y \in \mathcal S^-$
But $y \in Y$ was arbitrary, so we have: 
:$Y \subseteq \mathcal S^-$
So:
:$Y = \mathcal S^-$ 
That is: 
:$\mathcal S$ is everywhere dense in $Y$.
We now show that $\mathcal S$ is countable.
From Lexicographic Order on Pair of Well-Ordered Sets is Well-Ordering and the Well-Ordering Principle, there exists a well-order $\sqsubseteq$ on $\N \times \N$.
For each $y \in \mathcal S$, define a map $f : \mathcal S \to \N \times \N$ by picking $\map f y$ to be the $\sqsubseteq$-least element of $\set {y_{n, k} \in \mathcal S : y_{n, k} = y}$. 
Then $f$ is an injection.
From Cartesian Product of Countable Sets is Countable, $\N \times \N$ is countable.
So, from Domain of Injection to Countable Set is Countable, we have that: 
:$\mathcal S$ is countable.
So $\mathcal S$ is a countable everywhere dense subset of $Y$.
Category:Metric Spaces
Category:Separable Spaces
Subspace of Smooth Real Functions

== Corollary to Subspace of Real Functions of Differentiability Class ==
Let $\mathbb J = \set {x \in \R: a < x < b}$ be an open interval of the real number line $\R$.
Let $\map {C^\infty} {\mathbb J}$ denote the set of all continuous real functions on $\mathbb J$ which are differentiable on $\mathbb J$ at all orders.
Then $\struct {\map {C^\infty} {\mathbb J}, +, \times}_\R$ is a subspace of the $\R$-vector space $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Proof ==
Note that by the definition of smooth real function: 
:$\ds \map {C^\infty} {\mathbb J} = \bigcap_{m \mathop = 0}^\infty \map {C^m} {\mathbb J}$
By Subspace of Real Functions of Differentiability Class:
:$\struct {\map {C^m} {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$ for all $m$. 
Then, from Set of Linear Subspaces is Closed under Intersection:
:$\ds \struct {\map {C^\infty} {\mathbb J}, +, \times}_\R$ is a subspace of $\struct {\R^{\mathbb J}, +, \times}_\R$.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.5$
Category:Vector Subspaces
Category:Analysis
Subspace of Subspace is Subspace

== Theorem ==
Let $T = \struct{S, \tau}$ be a topological space.
Let $H \subseteq S$ be a non-empty subset of $S$ and $\tau_H$ be the subspace topology on $H$.
Let $K \subseteq S$ be a non-empty subset of $S$.
Then the subspace topology on $K$ induced by $\tau$ equals the subspace topology on $K$ induced by $\tau_H$.
== Proof ==
Let $\tau_K$ be the subspace topology on $K$ induced by $\tau$.
Let $\tau'_K$ be the subspace topology on $K$ induced by $\tau_H$.
Then
== Sources ==
* : $\S 3$: New Spaces From Old: Subspaces
Category:Topological Subspaces
Subspaces of Dimension 2 Real Vector Space

== Theorem ==
Take the $\R$-vector space $\left({\R^2, +, \times}\right)_\R$.
Let $S$ be a subspace of $\left({\R^2, +, \times}\right)_\R$.
Then $S$ is one of:
: $(1): \quad \left({\R^2, +, \times}\right)_\R$
: $(2): \quad \left\{{0}\right\}$
: $(3): \quad$ A line through the origin.
== Proof 1 ==
== Proof 2 ==
Category:Linear Algebra
Category:Subspaces of Dimension 2 Real Vector Space
Subspaces of Dimension 2 Real Vector Space/Proof 1

== Theorem ==
== Proof ==
Let $S$ be a non-zero subspace of $\struct {\R^2, +, \times}_\R$.
Then $S$ contains a non-zero vector $\tuple {\alpha_1, \alpha_2}$.
Hence $S$ also contains $\set {\lambda \times \tuple {\alpha_1, \alpha_2}, \lambda \in \R}$.
From Equation of Straight Line in Plane, this set may be described as a line through the origin.
Suppose $S$ also contains a non-zero vector $\tuple {\beta_1, \beta_2}$ which is not on that line.
Then:
:$\alpha_1 \times \beta_2 - \alpha_2 \times \beta_1 \ne 0$
Otherwise $\tuple {\beta_1, \beta_2}$ would be $\zeta \times \tuple {\alpha_1, \alpha_2}$, where either $\zeta = \beta_1 / \alpha_1$ or $\zeta = \beta_2 / \alpha_2$ according to whether $\alpha_1 \ne 0$ or $\alpha_2 \ne 0$.
But then $S = \struct {\R^2, +, \times}_\R$.
Because, if $\tuple {\gamma_1, \gamma_2}$ is any vector at all, then:
:$\tuple {\gamma_1, \gamma_2} = \lambda \times \tuple {\alpha_1, \alpha_2} + \mu \times \tuple {\beta_1, \beta_2}$
where:
:$\lambda = \dfrac {\gamma_1 \times \beta_2 - \gamma_2 \times \beta_1} {\alpha_1 \times \beta_2 - \alpha_2 \times \beta_1}, \mu = \dfrac {\alpha_1 \times \gamma_2 - \alpha_2 \times \gamma_1} {\alpha_1 \times \beta_2 - \alpha_2 \times \beta_1}$
which we get by solving the simultaneous equations:
The result follows.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 27$. Subspaces and Bases: Example $27.2$
Category:Subspaces of Dimension 2 Real Vector Space
Substitution/Examples/Arbitrary Example 1

== Example of Substitution ==
Consider the expression:
:$x^2 + 2 x + 6$
Substituting $2$ for $x$, we get:
:$2^2 + 2 \times 2 + 6$
which evaluates to $14$.
This is called making the substitution $x = 2$.
If instead we making the substitution $x = y - 1$, the expression becomes:
:$\paren {y - 1}^2 + 2 \paren {y - 1} + 6$
which simplifies to:
:$y^2 + 5$
It is now easily seen that the expression cannot be less than $5$ in value, which happens when $y = 0$.
That is, when $x = -1$.
== Sources ==
* 
* 
Category:Examples of Substitution
Substitution Instance of Term is Term

== Theorem ==
Let $\beta, \tau$ be terms of predicate logic.
Let $x \in \operatorname {VAR}$ be a variable.
Let $\map \beta {x \gets \tau}$ be the substitution instance of $\beta$ substituting $\tau$ for $x$.
Then $\map \beta {x \gets \tau}$ is a term.
== Proof ==
Proceed by the Principle of Structural Induction on the definition of term, applied to $\beta$.
If $\beta = y$ for some variable $y$, then:
:$\map \beta {x \gets \tau} = \begin{cases} \tau & : \text {if $y = x$} \\ y &: \text {otherwise} \end{cases}$
In either case, $\map \beta {x \gets \tau}$ is a term.
If $\beta = \map f {\tau_1, \ldots, \tau_n}$ and the induction hypothesis holds for $\tau_1, \ldots, \tau_n$, then:
:$\map \beta {x \gets \tau} = \map f {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} }$
By the induction hypothesis, each $\map {\tau_i} {x \gets \tau}$ is a term.
Hence so is $\map \beta {x \gets \tau}$.
The result follows by the Principle of Structural Induction.
== Sources ==
* : $\mathrm{II}.8$ Further Semantic Notions
Category:Predicate Logic
Substitution Instance of WFF is WFF

== Theorem ==
Let $\mathbf A$ be a WFF of predicate logic.
Let $\tau$ be a term of predicate logic.
Let $x \in \mathrm{VAR}$ be a variable.
Let $\mathbf A \left({x \gets \tau}\right)$ be the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.
Then $\mathbf A \left({x \gets \tau}\right)$ is a WFF.
== Proof ==
Proceed by the Principle of Structural Induction on the bottom-up specification of predicate logic, applied to $\mathbf A$.
If $\mathbf A = p \left({\tau_1, \ldots, \tau_n}\right)$, then:
:$\mathbf A \left({x \gets \tau}\right) = p \left({\tau_1 \left({x \gets \tau}\right), \ldots, \tau_n \left({x \gets \tau}\right)}\right)$
where $\tau_i \left({x \gets \tau}\right)$ is the substitution instance of $\tau_i$.
By Substitution Instance of Term is Term, each such $\tau_i \left({x \gets \tau}\right)$ is again a term.
It follows that $\mathbf A \left({x \gets \tau}\right)$ is again a WFF.
If $\mathbf A = \neg \mathbf B$ and the induction hypothesis applies to $\mathbf B$, then:
:$\mathbf A \left({x \gets \tau}\right) = \neg \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \mathbf B \circ \mathbf B'$ for $\circ$ one of $\land, \lor, \implies, \iff$ and the induction hypothesis applies to $\mathbf B, \mathbf B'$:
:$\mathbf A \left({x \gets \tau}\right) = \mathbf B \left({x \gets \tau}\right) \circ \mathbf B' \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \exists x: \mathbf B$, and the induction hypothesis applies to $\mathbf B$:
:$\mathbf A \left({x \gets \tau}\right) = \exists x: \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \forall x : \mathbf B$, and the induction hypothesis applies to $\mathbf B$:
:$\mathbf A \left({x \gets \tau}\right) = \forall x: \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
The result follows by the Principle of Structural Induction.
== Sources ==
* : $\mathrm{II}.8$ Further Semantic Notions
Category:Predicate Logic
Substitution Rule for Matrices

== Theorem ==
Let $\mathbf A$ be a square matrix of order $n$.
Then:
:$(1): \quad \ds \sum_{j \mathop = 1}^n \delta_{i j} a_{j k} = a_{i k}$
:$(2): \quad \ds \sum_{j \mathop = 1}^n \delta_{i j} a_{k j} = a_{k i}$
where:
:$\delta_{i j}$ is the Kronecker delta
:$a_{j k}$ is element $\tuple {j, k}$ of $\mathbf A$.
=== Using Einstein Summation Convention ===
== Proof ==
By definition of Kronecker delta:
:$\delta_{i j} = \begin {cases} 1 & : i = j \\ 0 & : i \ne j \end {cases}$
Thus:
:$\delta_{i j} a_{j k} = \begin {cases} a_{i k} & : i = j \\ 0 & : i \ne j \end {cases}$
and:
:$\delta_{i j} a_{k j} = \begin {cases} a_{k i} & : i = j \\ 0 & : i \ne j \end {cases}$
from which the result follows.
== Sources ==
* : $2.1$: Matrices: $(2.6)$
Category:Matrix Algebra
Substitution Rule for Matrices/Einstein Summation Convention

== Summation Convention ==
Let $\mathbf A$ be a square matrix of order $n$.
The Substitution Rule for Matrices can be expressed using the Einstein summation convention as:
:$(1): \quad \delta_{i j} a_{j k} = a_{i k}$
:$(2): \quad \delta_{i j} a_{k j} = a_{k i}$
where:
:$\delta_{i j}$ is the Kronecker delta
:$a_{j k}$ is element $\tuple {j, k}$ of $\mathbf A$.
The index which appears twice in these expressions is the element $j$, which is the one summated over.
== Sources ==
* : $2.2$: The summation convention
Category:Matrix Algebra