avewright/proofwiki-math huggingface dataset:
Theorem: Bochner Integral is Additive

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $I$ be a real interval.
Let $\lambda$ be the Lebesgue measure on $I$. 
Let $f, g : I \to X$ be Bochner integrable functions.
Then $f + g$ is Bochner integrable and:
:$\ds \int \paren {f + g} \rd \lambda = \int f \rd \lambda + \int g \rd \lambda$

Proof:
Let $\sequence {u_n}_{n \mathop \in \N}$ be a sequence of simple functions such that:
:$\map {u_n} t \to \map f t$ for each $t \in I \setminus N_1$, $\map \lambda {N_1} = 0$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {f - u_n}_X \rd \lambda = 0$
Then:
:$\ds \int_I f \rd \lambda = \lim_{n \mathop \to \infty} \int_I u_n \rd \lambda$ 
Let $\sequence {v_n}_{n \mathop \in \N}$ be a sequence of simple functions such that:
:$\map {v_n} t \to \map f t$ for each $t \in I \setminus N_2$, $\map \lambda {N_2} = 0$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {g - v_n}_X \rd \lambda = 0$
Then:
:$\ds \int_I g \rd \lambda = \lim_{n \mathop \to \infty} \int_I v_n \rd \lambda$ 
From Sum of Banach Space-Valued Simple Functions is Simple Function, $u_n + v_n$ is simple.
From Null Sets Closed under Countable Union, $N_1 \cup N_2$ is $\lambda$-null.
Further:
:$\map {u_n} t + \map {v_n} t \to \map f t + \map g t$ for each $t \in I \setminus \paren {N_1 \cup N_2}$.
We have:
{{begin-eqn}}
{{eqn	| l = \int_I \norm {\paren {f + g} - \paren {u_n + v_n} }_X \rd \lambda 
		| r = \int_I \norm {\paren {f - u_n} + \paren {g - v_n} }_X \rd \lambda 
}}
{{eqn	| o = \le
		| r = \int_I \norm {f - u_n}_X \rd \lambda + \int_I \norm {g - v_n}_X \rd \lambda 
		| c = {{NormAxiomVector|3}}, Integral of Integrable Function is Monotone and Integral of Integrable Function is Additive
}}
{{eqn	| o = \to 
		| r = 0
}}
{{end-eqn}}
Hence $f + g$ is Bochner integrable.
We then have:
{{begin-eqn}}
{{eqn	| l = \int_I \paren {f + g} \rd \lambda 
		| r = \lim_{n \mathop \to \infty} \int_I \paren {u_n + v_n} \rd \lambda 
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \paren {\int_I u_n \rd \lambda + \int_I v_n \rd \lambda}
		| c = Bochner Integral of Sum of Simple Functions
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \int_I u_n \rd \lambda + \lim_{n \mathop \to \infty} \int_I v_n \rd \lambda 
}}
{{eqn	| r = \int_I f \rd \lambda + \int_I g \rd \lambda 
}}
{{end-eqn}}
{{qed}}
Category:Bochner Integrals
5l24vld6tg6s39cwkge1yyjur3td29c
Theorem: Bochner Integral is Homogeneous

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $I$ be a real interval.
Let $\lambda$ be the Lebesgue measure on $I$. 
Let $f : I \to X$ be a Bochner integrable function.
Let $\alpha \in \GF$.
Then $\alpha f$ is Bochner integrable and:
:$\ds \int_I \paren {\alpha f} \rd \lambda = \alpha \int_I f \rd \lambda$

Proof:
Let $\sequence {u_n}_{n \mathop \in \N}$ be a sequence of simple functions such that:
:$\map {u_n} t \to \map f t$ for each $t \in I \setminus \Omega_0$, $\map \lambda {\Omega_0} = 0$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {f - u_n}_X \rd \lambda = 0$
Then:
:$\alpha \map {u_n} t \to \alpha \map f t$ for each $t \in I \setminus \Omega_0$
and:
{{begin-eqn}}
{{eqn	| l = \lim_{n \mathop \to \infty} \int_I \norm {\alpha f - \alpha u_n}_X \rd \lambda
		| r = \alpha \lim_{n \mathop \to \infty} \int_I \norm {f - u_n}_X \rd \lambda
		| c = {{NormAxiomVector|2}} 
}}
{{eqn	| r = 0
}}
{{end-eqn}}
Hence $\alpha f$ is Bochner integrable.
Further:
{{begin-eqn}}
{{eqn	| l = \int_I \paren {\alpha f} \rd \lambda 
		| r = \lim_{n \mathop \to \infty} \int \paren {\alpha u_n} \rd \lambda 
}}
{{eqn	| r = \alpha \lim_{n \mathop \to \infty} \int_I u_n \rd \lambda 
		| c = Integral of Integrable Function is Homogeneous
}}
{{eqn	| r = \alpha \int_I f \rd \lambda 
}}
{{end-eqn}}
{{qed}}
Category:Bochner Integrals
0iuy6nputgv3vmqjrtm44dcztgcxvgv
Theorem: Identity Natural Transformation is Natural Transformation

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F : \mathbf C \to \mathbf D$ be a covariant functor.
Let $\operatorname{id}_F: F \to F$ denote the identity natural transformation
Then:
:$\operatorname{id}_F$ is a natural transformation.

Proof:
{{Recall|Identity Natural Transformation|identity natural transformation}}
{{:Definition:Identity Natural Transformation}}
By definition of identity morphsim for all morphisms $f: X \to Y$ in $\mathbf C$:
:$\operatorname{id}_{FY} \circ Ff = Ff = Ff \circ \operatorname{id}_{FX}$
Hence for all morphisms $f: X \to Y$ in $\mathbf C$:
:$\paren{\operatorname{id}_F}_Y \circ Ff = Ff = Ff \circ \paren{\operatorname{id}_F}_X$
It follows that $\operatorname{id}_F$ is a natural transformation by definition.
{{qed}}
Category:Identity Natural Transformations
Category:Natural Transformations
qxvjhsvbil3nyoonmtie209hkn2wgrl
Theorem: Identity Natural Transformation is Left Identity

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation from $F$ to $G$.
Let $\operatorname{id}_G$ denote the identity natural transformation on $G$.
Then:
:$\operatorname{id}_G \mathop \circ \eta = \eta$
where $\operatorname{id}_G \mathop \circ \eta$ denotes the verictal composition of $\eta$ and $\operatorname{id}_G$.

Proof:
By definition of natural transformation for each object $X \in \mathbf C$:
:$\eta_X$ is a morphism from $F X$ to $G X$
such that for all objects $X, Y$ in $\mathbf C$ and for each morphism $f: X \to Y$ of $\mathbf C$:
:$\eta_Y \circ F f = G f \circ \eta_X$
For each object $X \in \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{\operatorname{id}_G \mathop \circ \eta}_X
      | r = \paren{\operatorname{id}_G}_X \mathop \circ \eta_X
      | c = {{Defof|Vertical Composition of Natural Transformations|Vertical Composition}}
}}
{{eqn | r = \paren{\operatorname{id}_{GX} } \mathop \circ \eta_X
      | c = {{Defof|Identity Natural Transformation}}
}}
{{eqn | r = \eta_X
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
It follows that:
:$\operatorname{id}_G \mathop \circ \eta = \eta$
{{qed}}
Theorem: Identity Natural Transformation is Right Identity

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ be a natural transformation from $F$ to $G$.
Let $\operatorname{id}_F$ denote the identity natural transformation on $F$.
Then:
:$\eta \circ \operatorname{id}_F = \eta$

Proof:
By definition of natural transformation for each object $X \in \mathbf C$:
:$\eta_X$ is a morphism from $F X$ to $G X$
such that for all objects $X, Y$ in $\mathbf C$ and for each morphism $f: X \to Y$ of $\mathbf C$:
:$\eta_Y \circ F f = G f \circ \eta_X$
For each object $X \in \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{\eta \circ \operatorname{id}_F}_X
      | r = \eta_X \circ \paren{\operatorname{id}_F}_X
      | c = {{Defof|Vertical Composition of Natural Transformations|Vertical Composition}}
}}
{{eqn | r = \eta_X \circ \paren{\operatorname{id}_{FX} }
      | c = {{Defof|Identity Natural Transformation}}
}}
{{eqn | r = \eta_X
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
It follows that:
:$\operatorname{id}_G \mathop \circ \eta = \eta$
{{qed}}
Theorem: Identity Natural Transformation is Idempotent

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F : \mathbf C \to \mathbf D$ be a covariant functor.
Let $\operatorname{id}_F$ denote the identity natural transformation on $F$.
Then:
:$\operatorname{id}_F \circ \operatorname{id}_F = \operatorname{id}_F$
where $\operatorname{id}_F \circ \operatorname{id}_F$ denotes the vertical composition of $\operatorname{id}_F$ with itself.

Proof:
For each object $X$ in $\mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{\operatorname{id}_F \circ \operatorname{id}_F}_X
      | r = \paren{\operatorname{id}_F}_X \circ \paren{\operatorname{id}_F}_X
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \operatorname{id}_{FX} \circ \operatorname{id}_{FX}
      | c = {{Defof|Identity Natural Transormation}}
}}
{{eqn | r = \operatorname{id}_{FX}
      | c = Identity Morphism is Idempotent
}}
{{eqn | r = \paren{\operatorname{id}_F}_X
      | c = {{Defof|Identity Natural Transormation}}
}}
{{end-eqn}}
It follows that:
:$\operatorname{id}_F \circ \operatorname{id}_F = \operatorname{id}_F$
{{qed}}
Category:Identity Natural Transformations
cyvlyfj1zkqgf3x0rliy1dq90zqugdr
Theorem: Identity Natural Transformation is Natural Isomorphism

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F : \mathbf C \to \mathbf D$ be a covariant functor.
Let $\operatorname{id}_F: F \to F$ denote the identity natural transformation
Then:
:$\operatorname{id}_F$ is a natural isomorphism

Proof:
By definition of identity natural transformation:
:for each $X \in \mathbf C : \paren{\operatorname{id}_F}_X = \operatorname{id}_{F X}$
where $\operatorname{id}_{F X}$ is the identity morphism on $F X$.
From Identity Morphism is Isomorphism:
:for each $X \in \mathbf C : \operatorname{id}_{F X}$ is an isomorphism of $\mathbf C$
Hence:
:for each $X \in \mathbf C : \paren{\operatorname{id}_F}_X$ is an isomorphism of $\mathbf C$
It follows that $\operatorname{id}_F$ is a natural isomorphism by definition.
{{qed}}
Category:Natural Isomorphisms
Category:Identity Natural Transformations
h5ml10jle1e7jq9ljkvowxr2me8jjt8
Theorem: Equivalence of Definitions of Adjunction

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$, $\mathbf D$ be locally small categories.
{{TFAE|def = Adjunction}}

Proof:
By definition of natural isomorphism
:$\alpha: \map {\mathrm {Hom}_{\mathbf C} } {F-, -} \to \map {\mathrm {Hom}_{\mathbf D} } {-, G-}$ is a natural isomorphism between:
::the hom bifunctor with left functor $\map {\mathrm {Hom}_{\mathbf C} } {F-, -} : \mathbf D^{\mathrm {op}} \times \mathbf C \to \mathbf{Set}$
:and:
::the hom bifunctor with right functor $\map {\mathrm {Hom}_{\mathbf D} } {-, G-} : \mathbf D^{\mathrm {op} } \times \mathbf C \to \mathbf{Set}$
{{iff}}
:for every object $\tuple{D^\text{op}, C}$ in $D^\text{op} \times C$:
::$\exists$ an isomorphism $\alpha_{\tuple{D^\text{op}, C}} \in \mathbf {Set}$
:such that for objects $\tuple{D_1^\text{op}, C_1}$ and $\tuple{D_2^\text{op}, C_2}$ and for morphism $\tuple{f^\text{op} : D_1^\text{op} \to D_2^\text{op}, g: C_1 \to C_2}$ in $D^\text{op} \times C$ we have:
::$\alpha_{\tuple{D_2^\text{op}, C_2}} \circ \map {\mathrm {Hom}_{\mathbf C} } {Ff^\text{op}, g} = \map {\mathrm {Hom}_{\mathbf C} } {f^\text{op}, Gg} \circ \alpha_{\tuple{D_1^\text{op}, C_1}}$
From Bijection Iff Isomorphism in Category of Sets:
:$\alpha_{\tuple{D_1^\text{op}, C_1}}$ is an isomorphism {{iff}} $\alpha_{\tuple{D_1^\text{op}, C_1}}$ is a bijection
By definition of hom bifunctor with left functor:
:$\map {\operatorname{Hom}_{\mathbf C}} {Ff^\text{op}, g} : \map {\operatorname{Hom}_{\mathbf C} } {FD_1, C_1} \to \map {\operatorname{Hom}_{\mathbf C} } {FD_2, C_2}$ is the mapping defined by : $h \mapsto g \circ h \circ Ff$
By definition of hom bifunctor with right functor:
:$\map {\operatorname{Hom}_{\mathbf D}} {f^\text{op}, Gg} : \map {\operatorname{Hom}_{\mathbf D} } {D_1, GC_1} \to \map {\operatorname{Hom}_{\mathbf D} } {D_2, GC_2}$ is the mapping defined by : $h \mapsto Gg \circ h \circ f$
The equivalence follows.
{{qed}}
Category:Adjunctions
1r3acsnf8fedhvzyenft3qsk3evwoaf
Theorem: Surjection iff Epimorphism in Category of Sets/Necessary Condition Proof 1

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a surjection.
Then:
:$f$ is an epimorphism in $\mathbf{Set}$.

Proof:
By definition of epimorphism:
:$f$ is an epimorphism
{{iff}}
:for all mappings $g, h: Y \to Z : g \circ f = h \circ f \implies g = h$
In the following we prove the contrapositive statement:
:for all mappings $g, h: Y \to Z : g \ne h \implies g \circ f \ne h \circ f$
Let $g, h: Y \to Z$ be mappings such that $g \ne h$.
From Equality of Mappings:
:$\exists y \in Y : \map g y \ne \map h y$
By definition of surjection:
:$(1) \quad \exists x \in X : \map f x = y$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren{g \circ f} } x
      | r = \map g {\map f x}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map g y
      | c = By $(1)$
}}
{{eqn | o = \ne
      | r = \map h y
      | c = {{hypothesis}}
}}
{{eqn | r = \map h {\map f x}
      | c = By $(1)$
}}
{{eqn | r = \map {\paren{h \circ f} } x
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
From Equality of Mappings:
:$g \circ f \ne h \circ f$.
By the Rule of Transposition:
:$f$ is epic.
Theorem: Surjection iff Epimorphism in Category of Sets/Necessary Condition Proof 2

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a surjection.
Then:
:$f$ is an epimorphism in $\mathbf{Set}$.

Proof:
Let $g, h: Y \to Z$ be mappings such that $g \circ f = h \circ f$.
Let $y \in Y$ be an arbitrary element of $Y$.
By definition of surjection:
:$(1) \quad \exists x \in X : \map f x = y$.
We have:
{{begin-eqn}}
{{eqn | l = \map g y
      | r = \map g {\map f x}
      | c = By $(1)$
}}
{{eqn | r = \map {\paren{g \circ f} } x
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\paren{h \circ f} } x
      | c = {{hypothesis}}
}}
{{eqn | r = \map h {\map f x}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map h y
      | c = By $(1)$
}}
{{end-eqn}}
Since $y$ was arbitrary we have:
:$\forall x \in X : \map g x = \map h x$.
From Equality of Mappings:
:$g = h$
Since $g$ and $h$ were arbitrary we have:
:$\forall g, h: Y \to Z : g \circ f = h \circ f \implies g = h$.
It follows that $f$ is epic by definition.
Theorem: Surjection iff Epimorphism in Category of Sets/Sufficient Condition

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be an epimorphism in $\mathbf{Set}$.
Then:
:$f$ is a surjection.

Proof:
The contrapositive statement will be proved, that is:
:if $f$ is not a surjection then $f$ is not an epimorphism.
The result will follow by the Rule of Transposition.
Let $f$ be not a surjection.
By definition of surjection:
:$\exists y_0 \in Y : \forall x \in X: \map f x \ne y_0$
Consider the mappings defined by:
:$g: Y \to Y \cup \set Y, \map g y := y$
:$h: Y \to Y \cup \set Y, \map h y := \begin{cases} y & \text{if } y \ne y_0 \\ Y & \text{if } y = y_0 \end{cases}$
By definition of $g$ and $h$:
:$\map g {y_0} = y_0 \ne Y = \map f {y_0}$
From Equality of Mappings:
:$g \ne h$
We have:
{{begin-eqn}}
{{eqn | q = \forall x \in X 
      | l = \map {\paren{h \circ f} } x
      | r = \map h {\map f x}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map f x
      | c = Definition of $h$ and since $\map f x \ne y_0$
}}
{{eqn | r = \map g {\map f x}
      | c = Definition of $g$
}}
{{eqn | r = \map {\paren{g \circ f} } x
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
From Equality of Mappings:
:$g \circ f = h \circ f$
It follows that $f$ is not an epimorphism by definition.
The result follows by Rule of Transposition.
Theorem: Bijection Iff Isomorphism in Category of Sets

Let $\mathbf{Set}$ be the category of sets.
Let $f: X \to Y$ be a morphism in $\mathbf{Set}$, i.e. a mapping.
Then:
:$f$ is a bijection {{iff}} it is an isomorphism in $\mathbf{Set}$.

Proof:
By definition of bijection:
:$f$ is a bijection 
{{iff}} 
:$f$ admits an inverse
By definition of inverse:
:$f$ admits an inverse 
{{iff}}
:$\exists$ a mapping $g: Y \to X : g \circ f = I_X \land f \circ g = I_Y$
where:
:$I_X$ and $I_Y$ denote the identity mappings on $X$ and $Y$ respectively.
By definition of category of sets:
:$\exists$ a mapping $g: Y \to X : g \circ f = I_X \land f \circ g = I_Y$
{{iff}}
:$\exists$ a morphism $g: Y \to X$ in $\mathbf{Set} : g \circ f = \operatorname{id}_X \land f \circ g = \operatorname{id}_Y$
where:
:$\operatorname{id}_X$ and $\operatorname{id}_Y$ denote the identity morphisms on $X$ and $Y$ respectively.
By definition of isomorphism:
:$\exists$ a morphism $g: Y \to X$ in $\mathbf{Set} : g \circ f = \operatorname{id}_X \land f \circ g = \operatorname{id}_Y$ 
{{iff}} 
:$f$ is an isomorphism in $\mathbf{Set}$
{{qed}}
Category:Bijections
Category:Category of Sets
n2jqu18nlknc2swqjyii6zdulsj7r4a
Theorem: Eccentricity of Ellipse in terms of Semiminor Axis and Linear Eccentricity

Let $K$ be a ellipse such that:
:$b$ denotes the length of semi-minor axis of $K$
:$c$ denotes the linear eccentricity of $K$
:$e$ denotes the eccentricity of $K$.
Then:
:$e = \dfrac c {\sqrt {b^2 + c^2} }$

Proof:
{{begin-eqn}}
{{eqn | l = e
      | r = \dfrac c a
      | c = Eccentricity of Ellipse is Linear Eccentricity over Semimajor Axis
}}
{{eqn | r = \dfrac c {\sqrt {b^2 + c^2} }
      | c = Linear Eccentricity of Ellipse from Major and Minor Axis: $a^2 = b^2 + c^2$
}}
{{end-eqn}}
{{qed}}
Category:Eccentricity of Ellipse
Category:Linear Eccentricity
Category:Semiminor Axis of Ellipse
Category:Ellipses
96twi9wga06chxycmrvnfbhxb0dzow5
Theorem: Coordinates of Foci of Ellipse in Reduced Form

Let $\KK$ be an ellipse embedded in a Cartesian plane in reduced form.
Then the foci of $\KK$ are at $\tuple {a e, 0}$ and $\tuple {-a e, 0}$, where:
:$a$ denotes the semimajor axis of $\KK$
:$e$ denotes the eccentricity of $\KK$.

Proof:
By definition of the reduced form of $\KK$:
:the major axis of $\KK$ coincides with the $x$-axis
:the center of $\KK$ coincides with the origin.
Hence the foci of $\KK$ are themselves situated on the $x$-axis, equidistant from the origin $\tuple {0, 0}$.
Let $c$ denote the linear eccentricity of $\KK$.
Thus, by definition of linear eccentricity, the foci of $\KK$ are situated at the points $\tuple {\pm c, 0}$.
From Eccentricity of Ellipse is Linear Eccentricity over Semimajor Axis, we have:
:$e = \dfrac c a$
from which the result follows.
{{qed}}
Theorem: Equations of Directrices of Ellipse in Reduced Form

Let $\KK$ be an ellipse embedded in a Cartesian plane in reduced form.
Then the directrices of $\KK$ are the lines:
:$x = \dfrac a e$
and:
:$x = -\dfrac a e$
where:
:$a$ denotes the semimajor axis of $\KK$
:$e$ denotes the eccentricity of $\KK$.

Proof:
By definition of the reduced form of $\KK$:
:the major axis of $\KK$ coincides with the $x$-axis
:the center of $\KK$ coincides with the origin.
By Directrix of Ellipse is Perpendicular to Major Axis, the directrices of $\KK$ are perpendicular to the $x$-axis.
Hence the equations of the directrices are in the form $x = \pm d$ for some $d$ to be found.
From Distance of Directrix of Ellipse from Center, we have that:
:$d = \dfrac a e$
and the result follows.
{{qed}}
Theorem: Identity Morphism is Idempotent

Let $\mathbf C$ be a category.
Let $X$ be an object of $\mathbf C$.
Let $\operatorname{id}_X : X \to X$ denote the identity morphism of $X$.
Then:
:$\operatorname{id}_X \circ \operatorname{id}_X = \operatorname{id}_X$

Proof:
By definition of identity morphism:
:for each object $Y \in \mathbf C$ and morphism $f : X \to Y$ in $\mathbf C$:
::$f \circ \operatorname{id}_X = f$
In particular, substituting $\operatorname{id}_X$ for $f$:
:$\operatorname{id}_X \circ \operatorname{id}_X = \operatorname{id}_X$
{{qed}}
Category:Morphisms
0h7c1ovv12jxsuan4o12rgcszuyfqv5
Theorem: Equivalence of Definitions of Natural Isomorphism between Covariant Functors

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
{{TFAE|def=Natural Isomorphism}}
=== Definition 1 ===
{{:Definition:Natural Isomorphism between Covariant Functors/Definition 1}}
=== Definition 2 ===
{{:Definition:Natural Isomorphism between Covariant Functors/Definition 2}}

Proof:
Let $\operatorname{id}_F$ and $\operatorname{id}_G$ denote the identity natural transformations of $F$ and $G$ respectively.
Theorem: Holomorphic Elliptic Function is Constant

Let $\phi: \C \to \C$ be an elliptic function.
Let $\phi$ in addition be a holomorphic function.
Then $\phi$ is constant

Proof:
{{tidy|minor stuff, good job}}
Let $\phi: \C \to \C$ be a holomorphic elliptic function.
Then there exist $\omega_1, \omega_2 \in \C$ such that:
:$\phi \paren z = \phi \paren {z + \omega_1} = \phi \paren {z + \omega_2}$
Let:
:$S = \set {a \omega_1 + b \omega_2 : a,b \in \closedint 0 1}$
Then $S$ is open and connected.
From the Maximum Modulus Principle on $\Int S$, there exists:
:$\ds M = \max_{z \mathop \in \partial S} \bigsize {\phi \paren z}$
such that:
:$\bigsize {\phi \paren z} \leq M \qquad \forall z \in S$
Hence $\phi$ is bounded on $S$.
Define a relation $\RR$ on $\C$ by:
:$w \mathrel \RR z \iff w-z = a \omega_1 + b \omega_2 \text{ for some } a, b \in \Z$
Observe that:
:$z \mathrel \RR w \implies \phi \paren z = \phi \paren w$
Since $\omega_1$ and $\omega_2$ are linearly independent over $\C$, it follows that:
:$\span \set {\omega_1,\omega_2} = \C$
Hence:
:$\forall z \in \C: \exists w \in S : w \mathrel \RR z$
Therefore:
:$\bigsize {\phi \paren z} = \bigsize {\phi \paren w} \leq M$
for every $z \in \C$.
Hence $\phi$ is bounded on $\C$.
Since $\phi$ is holomorphic, from Liouville's Theorem, $\phi$ is constant.
{{qed}}
Theorem: Equivalence of Definitions of Natural Isomorphism between Covariant Functors/Definition 1 Implies Definition 2

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta : F \to G$ be a natural transformation such that for all $X \in \mathbf C$, $\eta_X : FX \to GX$ is an isomorphism.
Then:
:$\eta$ is an an isomorphism from $F$ to $G$ in the functor category $\operatorname{Funct}(\mathbf C, \mathbf D)$, that is, there exists a natural transformation $\xi : G \to F$ such that the compositions $\xi \circ \eta = \operatorname{id}_F$ and $\eta \circ \xi = \operatorname{id}_G$ are identity natural transformations.

Proof:
By definition of isomorphism: 
:for each $X \in \mathbf C$ let $\xi_X : G X \to F X$ be the inverse of $\eta_X$
Let $f : Y \to X$ be a morphism of $\mathbf C$.
We have:
{{begin-eqn}}
{{eqn | l = \xi_X \circ Gf
      | r = \paren{\xi_X \circ Gf} \circ \operatorname{id}_{GY}
      | c = {{Defof|Identity Morphism}}
}}
{{eqn | r = \paren{\xi_X \circ Gf} \circ \paren{\eta_Y \circ \xi_Y}
      | c = {{Defof|Isomorphism (Category Theory)}}
}}
{{eqn | r = \xi_X \circ \paren{\paren{Gf \circ \eta_Y} \circ \xi_Y }
      | c = {{Defof|Metacategory|Associativity of Composition}} of metacateogry
}}
{{eqn | r = \xi_X \circ \paren{\paren{\eta_X \circ Ff} \circ \xi_Y }
      | c = {{Defof|Natural Transformation}} applied to $\eta$
}}
{{eqn | r = \paren{\xi_X \circ \eta_X} \circ \paren{Ff \circ \xi_Y }
      | c = {{Defof|Metacategory|Associativity of Composition}} of metacateogry
}}
{{eqn | r = \operatorname{id}_GX \circ \paren{Ff \circ \xi_Y }
      | c = {{Defof|Isomorphism (Category Theory)}}
}}
{{eqn | r = Ff \circ \xi_Y
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
Hence $\xi : G \to F$ is a natural transformation by definition.
For each $X \in \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{\xi \circ \eta}_X
      | r = \xi_X \circ \eta_X
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \operatorname{id}_{F X}
      | c = {{Defof|Isomorphism (Category Theory)}}
}}
{{eqn | r = \paren{\operatorname{id}_F}_X
      | c = {{Defof|Identity Natural Transformation}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \paren{\eta \circ \xi}_X
      | r = \eta_X \circ \xi_X
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \operatorname{id}_{G X}
      | c = {{Defof|Isomorphism (Category Theory)}}
}}
{{eqn | r = \paren{\operatorname{id}_G}_X
      | c = {{Defof|Identity Natural Transformation}}
}}
{{end-eqn}}
It follows that:
:$\xi \circ \eta = \operatorname{id}_F$
:$\eta \circ \xi = \operatorname{id}_G$
and hence $\eta : F \to G$ is an isomorphism in the functor category $\operatorname{Funct}(\mathbf C, \mathbf D)$ by definition.