avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of Natural Isomorphism between Covariant Functors/Definition 2 Implies Definition 1

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 $\eta$ is 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.
Then:
:$\eta : F \to G$ satisfies for all $X \in \mathbf C$, $\eta_X : FX \to GX$ is an isomorphism.

Proof:
For each $X \in \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \xi_X \circ \eta_X
      | r = \paren{\xi \circ \eta}_X
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \paren{\operatorname{id}_F}_X
      | c = {{Defof|Isomorphism (Category Theory)|Isomorphism}} 
}}
{{eqn | r = \operatorname{id}_{FX}
      | c = {{Defof|Identity Natural Transformation}} 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \eta_X \circ \xi_X
      | r = \paren{\eta \circ \xi}_X
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \paren{\operatorname{id}_G}_X
      | c = {{Defof|Isomorphism (Category Theory)|Isomorphism}} 
}}
{{eqn | r = \operatorname{id}_{GX}
      | c = {{Defof|Identity Natural Transformation}} 
}}
{{end-eqn}}
Hence $\eta_X$ is an isomorphism in $\mathbf D$ by definition.
Theorem: Identity Morphism is Isomorphism

Let $\mathbf C$ be a metacategory.
Let $X$ be an object in $\mathbf C$.
Then:
:the identity morphism $\operatorname{id}_X$ of $X$ is an isomorphism in $\mathbf C$.

Proof:
By definition of identity morphism:
:$\operatorname{dom} \operatorname{id}_X = X$
:$f \circ \operatorname{id}_X = f$
whenever $X$ is the domain of $f$.
In particular:
:$\operatorname{id}_X \circ \operatorname{id}_X = \operatorname{id}_X$
By definition of an isomorphism:
:a morphism $f: Y \to Z$ is an '''isomorphism''' {{iff}} there exists a morphism $g: Z \to Y$ such that:
::$g \circ f = \operatorname{id}_Y$
::$f \circ g = \operatorname{id}_Z$
It follows that $\operatorname{id}_X$ is an isomorphism by definition.
{{qed}}
Category:Isomorphisms (Category Theory)
qk9wzxjtmsf0pvf1hw6zlltra6dz4al
Theorem: Vertical Composition of Natural Transformations is Associative

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F_1, F_2, F_3, F_4 : \mathbf C \to \mathbf D$ be functors.
Let $\eta: F_1 \to F_2$, $\xi: F_2 \to F_3$ and $\alpha: F_3 \to F_4$ be natural transformations.
Then:
:$\paren {\alpha \circ \xi} \circ \eta = \alpha \circ \paren {\xi \circ \eta}$
where $\circ$ denotes vertical composition of natural transformations

Proof:
By definition of natural transformation:
:For every object $A$ of $\mathbf C$, we have morphisms of $\mathsf D$:
::$\eta_A: F_1 A \to F_2 A$
::$\xi_A: F_2 A \to F_3 A$
::$\alpha_A: F_3 A \to F_4 A$
We have:
{{begin-eqn}}
{{eqn | l = \paren {\paren {\alpha \circ \xi} \circ \eta}_A
      | r = \paren {\alpha \circ \xi}_A \circ \eta_A
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \paren {\alpha_A \circ \xi_A} \circ \eta_A
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \alpha_A \circ \paren {\xi_A \circ \eta_A}
      | c = associativity of composition in $\mathbf D$
}}
{{eqn | r = \alpha_A \circ \paren {\xi \circ \eta}_A
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \paren {\alpha \circ \paren {\xi \circ \eta} }_A
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{end-eqn}}
By definition of natural transformation:
:$\paren {\alpha \circ \xi} \circ \eta = \alpha \circ \paren {\xi \circ \eta}$
{{qed}}
Category:Natural Transformations
hfsplb8m2fw0fuy5d0ycstum25nly91
Theorem: Composition of Isomorphisms is Isomorphism

Let $\mathbf C$ be a metacategory.
Let $f: A \to B$ and $g: B \to C$ be isomorphisms with inverses $f^{-1}: B \to A$ and $g^{-1}: C \to B$ respectively.
Then:
:the composition $g \circ f: A \to C$ is an isomorphism with inverse $f^{-1} \circ g^{-1}: C \to A$.

Proof:
Let $\operatorname{id}_A, \operatorname{id}_B$ and $\operatorname{id}_C$ denote the identity morphisms of $A, B$ and $C$ respectively.
We have:
{{begin-eqn}}
{{eqn | l = \paren {f^{-1} \circ g^{-1} } \circ \paren {g \circ f}
      | r = \paren {f^{-1} \circ \paren {g^{-1} \circ g} } \circ f
      | c = Associativity of composition in $\mathbf C$
}}
{{eqn | r = \paren {f^{-1} \circ \operatorname{id}_B } \circ f
      | c = {{Defof|Inverse Morphism}}
}}
{{eqn | r = f^{-1} \circ f
      | c = {{Defof|Identity Morphism}}
}}
{{eqn | r = \operatorname{id}_A
      | c = {{Defof|Inverse Morphism}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \paren {g \circ f} \circ \paren {f^{-1} \circ g^{-1} }
      | r = \paren {g \circ \paren {f \circ f^{-1} } } \circ g^{-1}
      | c = Associativity of composition in $\mathbf C$
}}
{{eqn | r = \paren {g \circ \operatorname{id}_B } \circ g^{-1}
      | c = {{Defof|Inverse Morphism}}
}}
{{eqn | r = g \circ g^{-1}
      | c = {{Defof|Identity Morphism}}
}}
{{eqn | r = \operatorname{id}_C
      | c = {{Defof|Inverse Morphism}}
}}
{{end-eqn}}
It follows that $g \circ f$ is an isomorphism with inverse $f^{-1} \circ g^{-1}$ by definition.
{{qed}}
Category:Isomorphisms (Category Theory)
tlt5sorheh9xewbycpwm5v4fn2lb102
Theorem: Uncertainty is Maximal for Uniform Distribution

Let $X$ be a discrete probability distribution.
Let the uncertainty of $X$ be maximal.
Then $X$ is the (discrete) uniform distribution.

Proof:
From Axiom $1$ of the Axioms of Uncertainty:
{{:Axiom:Axioms of Uncertainty}}
$H_n$ fulfils the following axiom:
:$\map {H_n} {p_1, p_2, \ldots, p_n}$ is a maximum when $p_1 = p_2 = \dotsb = p_n = \dfrac 1 n$
The result follows.
{{qed}}
Theorem: Equivalence of Definitions of Affine Algebraic Variety

Let $k$ be a field.
Let $n \ge 1$ be an integer.
{{TFAE|def = Affine Algebraic Variety}}

Proof:
Let $X \subseteq k^n$ be an affine algebraic set.
Theorem: Product of Functors is Functor

Let $\mathbf C$, $\mathbf C'$, $\mathbf D$, $\mathbf D'$ be categories.
Let $F: \mathbf C \to \mathbf D$ and $G: \mathbf C' \to \mathbf D'$ be covariant functors.
Let $F \times G:\mathbf C \times \mathbf C' \to \mathbf D \times \mathbf D'$ denote the product of $F$ and $G$.
Then:
:$F \times G:\mathbf C \times \mathbf C' \to \mathbf D \times \mathbf D'$ is a covariant functor

Proof:
=== $F \times G$ Preserves Composite Morphsims ===
For any composable morphisms $\tuple{f_1, g_1}, \tuple{f_2, g_2} \in \mathbf C \times \mathbf C'$ we have:
{{begin-eqn}}
{{eqn | l = \map {\paren{F \times G} } {\tuple{f_2, g_2} \circ \tuple{f_1, g_1} }
      | r = \map {\paren{F \times G} } {f_2 \circ f_1, g_2 \circ g_1}
      | c = {{Defof|Product Category|Composition in Product Category}}
}}
{{eqn | r =  \tuple{\map F {f_2 \circ f_1}, \map G {g_2 \circ g_1} }
      | c = {{Defof|Product of Functors}}
}}
{{eqn | r =  \tuple{F f_2 \circ F f_1, G g_2 \circ G g_1}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r =  \tuple{F f_2, G g_2} \circ \tuple{F f_1, G g_1}
      | c = {{Defof|Product Category|Composition in Product Category}}
}}
{{eqn | r =  \map {\paren{F \times G} } {f_2, g_2} \circ \map {\paren{F \times G} } {f_1, g_1}
      | c = {{Defof|Product of Functors}}
}}
{{end-eqn}}
Hence $F \times G$ preserves composite morphisms.
{{qed|lemma}}
Theorem: Functor Induced on Opposite Categories

Let $\mathbf C$, $\mathbf D$ be categories.
Let $\mathbf C^\text{op}$, $\mathbf D^\text{op}$ denote the dual categories of $\mathbf C$, $\mathbf D$ respectively.
Let $F: \mathbf C \to \mathbf D$ be a covariant functor.
Let $F^\text{op}: \mathbf C^\text{op} \to \mathbf D^\text{op}$ be defined as:
{{DefineFunctor
|ob = for each object $C^\text{op} \in \mathbf C^\text{op} : \map {F^\text{op} }  {C^\text{op} } := \paren{F C}^\text{op}$
|mor = for each morphism $f^\text{op} \in \mathbf C^\text{op} : \map {F^\text{op} } {f^\text{op} } := \paren{F f}^\text{op}$
}}
Then:
:$F^\text{op}: \mathbf C^\text{op} \to \mathbf D^\text{op}$ is a covariant functor

Proof:
=== $F^\text{op}$ Preserves Composite Morphsims ===
For any composable morphisms $f_1^\text{op}, f_2^\text{op} \in \mathbf C^\text{op}$ we have:
{{begin-eqn}}
{{eqn | l = \map {F^\text{op} } {f_2^\text{op} \circ f_1^\text{op} }
      | r = \map {F^\text{op} } {\paren{f_1 \circ f_2}^\text{op} }
      | c = {{Defof|Dual Category|Composition in Dual Category}}
}}
{{eqn | r = \paren{\map F {f_1 \circ f_2} }^\text{op}
      | c = Definition of $F^\text{op}$
}}
{{eqn | r = \paren{F f_1 \circ F f_2}^\text{op}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r =  \paren{F f_2}^\text{op} \circ \paren{F f_1}^\text{op}
      | c = {{Defof|Dual Category|Composition in Dual Category}}
}}
{{eqn | r = \map {F^\text{op} } {f_2^\text{op} } \circ \map {F^\text{op} } {f_1^\text{op} }
      | c = Definition of $F^\text{op}$
}}
{{end-eqn}}
Hence $F^\text{op}$ preserves composite morphisms.
{{qed|lemma}}
Theorem: Equations of Motion with Constant Acceleration/Distance after Time in terms of Velocities

:$\mathbf s = \dfrac {\paren {\mathbf u + \mathbf v} t} 2$

Proof:
From Equations of Motion with Constant Acceleration: Velocity after Time:
:$(1): \quad \mathbf v = \mathbf u + \mathbf a t$
From Equations of Motion with Constant Acceleration: Distance after Time:
:$(2): \quad \mathbf s = \mathbf u t + \dfrac {\mathbf a t^2} 2$
Hence:
{{begin-eqn}}
{{eqn | n = 3
      | l = \mathbf v - \mathbf u
      | r = \mathbf a t
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \mathbf s
      | r = \mathbf u t + \dfrac {\paren {\mathbf v - \mathbf u} t} 2
      | c = substituting for $\mathbf a t$ from $(3)$ in $(2)$
}}
{{eqn | r = \dfrac {\paren {\mathbf u + \mathbf v} t} 2
      | c = after algebra
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Bifunctor Induced By One-Variable Functors

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
Let $F_0: \mathbf C_0 \times \mathbf D_0 \to \mathbf E_0$ be an object functor.
Let $F_1: \mathbf C_1 \times \mathbf D_1 \to \mathbf E_1$ be a morphism functor.
For each $C \in \mathbf C_0$, let:
:$\paren{L_C}_0: \mathbf D_0 \to \mathbf E_0$ denote the object functor defined by:
::For each $D \in \mathbf D_0 : \map {\paren{L_C}_0} D = \map {F_0} {C, D}$
:$\paren{L_C}_1: \mathbf D_1 \to \mathbf E_1$ denote the morphism functor defined by:
::For each $g \in \mathbf D_1 : \map {\paren{L_C}_1} g = \map {F_1} {\operatorname{id}_C, g}$
For each $D \in \mathbf D_0$, let:
:$\paren{M_D}_0: \mathbf C_0 \to \mathbf E_0$ denote the object functor defined by:
::For each $C \in \mathbf C_0 : \map {\paren{M_D}_0} C = \map {F_0} {C, D}$
:$\paren{M_D}_1: \mathbf C_1 \to \mathbf E_1$ denote the morphism functor defined by:
::For each $f \in \mathbf C_1 : \map {\paren{M_D}_1} f = \map {F_1} {f, \operatorname{id}_D}$
Then:
:$F$ is a bifunctor 
{{iff}}:
{{begin-axiom}}
{{axiom | n = 1
        | lc = '''Functor in First Variable''': 
        | t = for each object $D \in \mathbf D : M_D: \mathbf C \to \mathbf E$ is a covariant functor
}}
{{axiom | n = 2
        | lc = '''Functor in Second Variable''': 
        | t = for each object $C \in \mathbf C : L_C: \mathbf D \to \mathbf E$ is a covariant functor
}}
{{axiom | n = 3
        | lc = '''Interchange Law''': 
        | t = for morphisms $f: C \to C' \in \mathbf C$ and $g: D \to D' \in \mathbf D : \map {M_{D'} } f \circ \map {L_C} g = \map {L_{C'} } g \circ \map {M_D} f = \map F {f, g}$
}}
{{end-axiom}}
The '''Interchange Law''' states that the following diagram commutes:
::<nowiki>$\begin{xy}
<-6em,0em>*+{\map F {C, D} } = "FCD",
<6em,0em>*+{\map F {C, D'} } = "FCD2",
<-6em,-6em>*+{\map F {C', D} } = "FC2D",
<6em,-6em>*+{\map F {C', D'} } = "FC2D2",
"FCD";"FCD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\map {L_C} g},
"FC2D";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\map {L_{C'} } g},
"FCD";"FC2D" **@{-} ?>*@{>} ?<>(.5)*!/^2em/{\map {M_D} f},
"FCD2";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/_2em/{\map {M_{D'} } f},
"FCD";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\map F {f, g} },
\end{xy}$</nowiki>

Proof:
=== Necessary Condition ===
Let $F$ be a bifunctor.
{{:Characterization of Bifunctor Induced By One-Variable Functors/Necessary Condition|Necessary Condition}}{{qed|lemma}}
Theorem: Characterization of Natural Transformation Between Bifunctors

Let $\mathbf C, \mathbf D$ and $\mathbf E$ be categories.
Let $F, G : \mathbf C \times \mathbf D \to \mathbf E$ be bifunctors from the product category $\mathbf C \times \mathbf D$ to the category $\mathbf E$.
For each object $C \in\mathbf C$ let: 
:$F \tuple{C, -}$ and $G \tuple{C, -}$
denote the functors obtained by substituting the first variable of $F$ and $G$, respectively, with $C$.
For each object $D \in\mathbf D$ let:
:$F \tuple{-, D}$ and $G \tuple{-, D}$
denote the functors obtained by substituting the second variable of $F$ and $G$, respectively, with $D$.
For each object $\tuple{C, D} \in \mathbf C \times \mathbf D$ let:
:$\alpha_{\tuple{C, D}} : F \tuple{C,D} \to G \tuple{C,D}$ 
denote a morphism in $\mathbf E$.
Then:
:$\alpha : F \to G$ is a natural transformation
{{iff}}
:$(1)\quad$ For each object  $C \in \mathbf C : \alpha \tuple{C, -} : F \tuple{C, -} \to G \tuple{C, -}$ is a natural transformation
:$(2)\quad$ For each object  $D \in \mathbf D : \alpha \tuple{-, D} : F \tuple{-, D} \to G \tuple{-, D}$ is a natural transformation
where:
:for objects $C \in \mathbf C$ and $D \in \mathbf D$, $\alpha \tuple{C, -}_D = \alpha_{\tuple{C, D}}$
and:
:for objects $C \in \mathbf C$ and $D \in \mathbf D$, $\alpha \tuple{-, D}_C = \alpha_{\tuple{C, D}}$

Proof:
=== Necessary Condition ===
Let $\alpha : F \to G$ be a natural transformation.
{{:Characterization of Natural Transformation Between Bifunctors/Proof 1 Necessary Condition}}{{qed|lemma}}
=== Sufficient Condition ===
Let:
:$(1)\quad$ For each object  $C \in \mathbf C : \alpha \tuple{C, -} : F \tuple{C, -} \to G \tuple{C, -}$ be a natural transformation
:$(2)\quad$ For each object  $D \in \mathbf D : \alpha \tuple{-, D} : F \tuple{-, D} \to G \tuple{-, D}$ be a natural transformation
{{:Characterization of Natural Transformation Between Bifunctors/Proof 1 Sufficient Condition}}{{qed}}
Theorem: Characterization of Natural Transformation Between Bifunctors

Let $\mathbf C, \mathbf D$ and $\mathbf E$ be categories.
Let $F, G : \mathbf C \times \mathbf D \to \mathbf E$ be bifunctors from the product category $\mathbf C \times \mathbf D$ to the category $\mathbf E$.
For each object $C \in\mathbf C$ let: 
:$F \tuple{C, -}$ and $G \tuple{C, -}$
denote the functors obtained by substituting the first variable of $F$ and $G$, respectively, with $C$.
For each object $D \in\mathbf D$ let:
:$F \tuple{-, D}$ and $G \tuple{-, D}$
denote the functors obtained by substituting the second variable of $F$ and $G$, respectively, with $D$.
For each object $\tuple{C, D} \in \mathbf C \times \mathbf D$ let:
:$\alpha_{\tuple{C, D}} : F \tuple{C,D} \to G \tuple{C,D}$ 
denote a morphism in $\mathbf E$.
Then:
:$\alpha : F \to G$ is a natural transformation
{{iff}}
:$(1)\quad$ For each object  $C \in \mathbf C : \alpha \tuple{C, -} : F \tuple{C, -} \to G \tuple{C, -}$ is a natural transformation
:$(2)\quad$ For each object  $D \in \mathbf D : \alpha \tuple{-, D} : F \tuple{-, D} \to G \tuple{-, D}$ is a natural transformation
where:
:for objects $C \in \mathbf C$ and $D \in \mathbf D$, $\alpha \tuple{C, -}_D = \alpha_{\tuple{C, D}}$
and:
:for objects $C \in \mathbf C$ and $D \in \mathbf D$, $\alpha \tuple{-, D}_C = \alpha_{\tuple{C, D}}$

Proof:
=== Necessary Condition ===
Let $\alpha : F \to G$ be a natural transformation.
{{:Characterization of Natural Transformation Between Bifunctors/Proof 2 Necessary Condition}}{{qed|lemma}}
=== Sufficient Condition ===
Let:
:$(1)\quad$ For each object  $C \in \mathbf C : \alpha \tuple{C, -} : F \tuple{C, -} \to G \tuple{C, -}$ be a natural transformation
:$(2)\quad$ For each object  $D \in \mathbf D : \alpha \tuple{-, D} : F \tuple{-, D} \to G \tuple{-, D}$ be a natural transformation
{{:Characterization of Natural Transformation Between Bifunctors/Proof 2 Sufficient Condition}}{{qed}}
Theorem: Circle is Locus of Equidistant Points from Point in Plane

Let $P$ be a point in the plane.
The locus of points which are equidistant from $P$ is the circle whose center is $P$.

Proof:
{{Recall|Circle}}
:{{Definition:Circle}}
The result follows directly.
{{qed}}
Theorem: Sphere is Locus of Equidistant Points from Point in Space

Let $P$ be a point in space.
The locus of points which are equidistant from $P$ is the sphere whose center is $P$.

Proof:
{{Recall|Sphere (Geometry)}}
:{{Definition:Sphere (Geometry)}}
The result follows directly.
{{qed}}
Theorem: Rhombus is Equilateral but not Equiangular

Let $\Box ABCD$ be a rhombus.
Then while $\Box ABCD$ is equilateral, it is not generally the case that $\Box ABCD$ is also equiangular.
If $\Box ABCD$ is also equiangular, then it is a square

Proof:
{{Recall|Rhombus|rhombus}}
{{:Definition:Rhombus}}
{{Recall|Square (Geometry)|square}}
{{:Definition:Square (Geometry)}}
The result follows.
{{qed}}
Theorem: Equivalence Classes with Common Element are Equal

Let $\RR$ be an equivalence relation on a set $S$.
Let $\eqclass x \RR$ and $\eqclass y \RR$ denote the $\RR$-equivalence classes of $x$ and $y$ respectively.
Let $z \in S$ such that $z \in \eqclass x \RR$ and $z \in \eqclass y \RR$.
Then:
:$\eqclass x \RR = \eqclass y \RR$

Proof:
Let $z \in S$ such that $z \in \eqclass x \RR$ and $z \in \eqclass y \RR$ {{hypothesis}}.
By definition of set intersection:
:$z \in \eqclass x \RR \cap \eqclass y \RR$
{{AimForCont}} $\eqclass x \RR \ne \eqclass y \RR$.
From Equivalence Classes are Disjoint:
:$\eqclass x \RR \cap \eqclass y \RR = \O$
But this contradicts:
:$z \in \eqclass x \RR \cap \eqclass y \RR$
Hence by Proof by Contradiction it cannot be the case that $\eqclass x \RR \ne \eqclass y \RR$.
The result follows.
{{qed}}
Theorem: Characterization of Bifunctor Induced By One-Variable Functors/Sufficient Condition

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
Let $F_0: \mathbf C_0 \times \mathbf D_0 \to \mathbf E_0$ be an object functor.
Let $F_1: \mathbf C_1 \times \mathbf D_1 \to \mathbf E_1$ be a morphism functor.
For each $C \in \mathbf C_0$, let:
:$\paren{L_C}_0: \mathbf D_0 \to \mathbf E_0$ denote the object functor defined by:
::For each $D \in \mathbf D_0 : \paren{L_C}_0 D = F_0 \tuple{C, D}$
:$\paren{L_C}_1: \mathbf D_1 \to \mathbf E_1$ denote the morphism functor defined by:
::For each $g \in \mathbf D_1 : \paren{L_C}_1 g = F_1 \tuple{\operatorname{id}_C, g}$
For each $D \in \mathbf D_0$, let:
:$\paren{M_D}_0: \mathbf C_0 \to \mathbf E_0$ denote the object functor defined by:
::For each $C \in \mathbf C_0 : \paren{M_D}_0 C = F_0 \tuple{C, D}$
:$\paren{M_D}_1: \mathbf C_1 \to \mathbf E_1$ denote the morphism functor defined by:
::For each $f \in \mathbf C_1 : \paren{M_D}_1 f = F_1 \tuple{f, \operatorname{id}_D}$
Let:
:$(1) :$ for each object $D \in \mathbf D : M_D: \mathbf C \to \mathbf E$ be a covariant functor
:$(2) :$ for each object $C \in \mathbf C : L_C: \mathbf D \to \mathbf E$ be a covariant functor
:$(3) :$ for each $f: C \to C' \in \mathbf C$ and $g: D \to D' \in \mathbf D : \paren{M_{D'} } f \circ \paren{L_C} g = \paren{L_{C'} } g \circ \paren{M_D} f = F \tuple{f, g}$
Then:
:$F$ is a bifunctor

Proof:
For morphisms:
:$\tuple{f : C \to C', g : D \to D'}, \tuple{f' : C' \to C' ', g' : D' \to D' '} \in \mathbf C \times \mathbf D$
we have:
{{begin-eqn}}
{{eqn | l = F \paren{\tuple{f', g'} \circ \tuple{f, g} }
      | r = F \tuple{f' \circ f, g' \circ g}
      | c = {{Defof|Product Category|Composition in Product Category}}
}}
{{eqn | r = \map {M_{D' '} } {f' \circ f} \circ \map {L_C} {g' \circ g}
      | c = By $(3)$
}}
{{eqn | r = \map {M_{D' '} } {f'} \circ \map {M_{D' '} } f  \circ \map {L_C} {g'} \circ \map {L_C} g
      | c = By $(1)$ and $(2)$
}}
{{eqn | r = \map {M_{D' '} } {f'} \circ \map {L_{C'} } {g'}  \circ \map {M_{D'} } f \circ \map {L_C} g
      | c = By $(3)$
}}
{{eqn | r = F \tuple{f', g'} \circ F \tuple{f, g}
      | c = By $(3)$
}}
{{end-eqn}}
Hence $F$ preserves composition of morphisms.
For object:
:$\tuple{C, D} \in \mathbf C \times \mathbf D$
we have:
{{begin-eqn}}
{{eqn | l = F \operatorname{id}_{\tuple{C, D} }
      | r = F \tuple{\operatorname{id}_C, \operatorname{id}_D}
      | c = {{Defof|Product Category|Identity Morphism in Product Category}}
}}
{{eqn | r = \map {M_D } {\operatorname{id}_C} \circ \map {L_C} {\operatorname{id}_D}
      | c = By $(3)$
}}
{{eqn | r = \operatorname{id}_{M_D C} \operatorname{id}_{L_C D}
      | c = By $(1)$ and $(2)$
}}
{{eqn | r = \operatorname{id}_{F \tuple{C, D} } \circ \operatorname{id}_{F \tuple{C, D} }
      | c = Definition of $M_D$ and $L_C$
}}
{{eqn | r = \operatorname{id}_{F \tuple{C, D} }
      | c = Identity Morphism is Idempotent
}}
{{end-eqn}}
Hence $F$ preserves identity morphisms.
It follows that $F$ is a bifunctor by definition.
Theorem: Characterization of Existence of Bifunctor Induced By One-Variable Functors

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
For each object $C \in \mathbf C$, let:
:$L_C: \mathbf D \to \mathbf E$ be a covariant functor.
For each object $D \in \mathbf D$, let:
:$M_D: \mathbf C \to \mathbf E$  be a covariant functor.
Then:
:there exists a bifunctor $F: \mathbf C \times \mathbf D \to \mathbf E$ such that:
::$(1)\quad$ For each object $C \in \mathbf C : F(C, -) = L_C$
::$(2)\quad$ For each object $D \in \mathbf D : F(-, D) = M_D$
:where:
::$F(C, -)$ denotes the functor from $\mathbf D$ to $\mathbf E$ obtained by substitution of first variable with $C$
::$F(-, D)$ denotes the functor from $\mathbf C$ to $\mathbf E$ obtained by substitution of second variable with $D$
{{iff}}:
{{begin-axiom}}
{{axiom | lc = '''Interchange Law''': 
        | t = for morphisms $f: C \to C' \in \mathbf C$ and $g: D \to D' \in \mathbf D : \map {M_{D'} } f \circ \map {L_C} g = \map {L_{C'} } g \circ \map {M_D} f$
}}
{{end-axiom}}
The '''Interchange Law''' states that the following diagram commutes:
::<nowiki>$\begin{xy}
<-8em,0em>*+{\map F {C, D} } = "FCD",
<8em,0em>*+{\map F {C, D'} } = "FCD2",
<-8em,-6em>*+{\map F {C', D} } = "FC2D",
<8em,-6em>*+{\map F {C', D'} } = "FC2D2",
"FCD";"FCD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\map {L_C} g = \map F {C, g} },
"FC2D";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\map {L_{C'} } g = \map F {C', g} },
"FCD";"FC2D" **@{-} ?>*@{>} ?<>(.5)*!/^5em/{\map {M_D} f = \map F {f, D} },
"FCD2";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/_5em/{\map {M_{D'} } f = \map F {f, D'} },
"FCD";"FC2D2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\map F {f, g} },
\end{xy}$</nowiki>

Proof:
=== Necessary Condition ===
Let $F: \mathbf C \times \mathbf D \to \mathbf E$ be a bifunctor such that:
::$(1)\quad$ For each object $C \in \mathbf C : F(C, -) = L_C$
::$(2)\quad$ For each object $D \in \mathbf D : F(-, D) = M_D$
{{:Characterization of Existence of Bifunctor Induced By One-Variable Functors/Necessary Condition|Necessary Condition}}{{qed|lemma}}