Theorem: Characterization of Hom Bifunctor with Left Functor as Composition of Functors

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$ be a locally small category.
Let $\mathbf D$ be a locally small category.
Let $L : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\map {\operatorname{Hom}_{\mathbf C} } {L-, -} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor with left functor.
Then:
:$\map {\operatorname{Hom}_{\mathbf C} } {L-, -} = \map {\operatorname{Hom}_{\mathbf C} } {-, -} \circ \paren{L^\text{op} \times \operatorname{id}_{\mathbf C} }$
where:
:* $L^\text{op}$ is the covariant functor $L^\text{op}: C^\text{op} \to D^\text{op}$ defined by:
:::Object functor: for each object $C \in \mathbf C^\text{op} : \map {F^\text{op} } C := \paren{F C}^\text{op}$
:::Morphism functor: for each morphism $f \in \mathbf C^\text{op} : \map {F^\text{op} } f := \paren{F f}^\text{op}$
:* $\operatorname{id}_{\mathbf C}$ denotes the identity functor on $\mathbf C$
:* $L^\text{op} \times \operatorname{id}_{\mathbf C}$ denotes the product of functors $L^\text{op}$ and $\operatorname{id}_{\mathbf C}$
:* $\map {\operatorname{Hom}_{\mathbf C} } {-, -}$ denotes the hom bifunctor $\map {\operatorname{Hom}_{\mathbf C} } {-, -} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$
:* $\map {\operatorname{Hom}_{\mathbf C} } {-, -} \circ \paren{L^\text{op} \times \operatorname{id}_{\mathbf C} }$ is the composition of $\paren{L^\text{op} \times \operatorname{id}_{\mathbf C} }$ with $\map {\operatorname{Hom}_{\mathbf C} } {-, -}$

Proof:
Let $F$ denote the hom bifunctor with left functor $\map {\operatorname{Hom}_{\mathbf C} } {L-, -} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$.
Let $G$ denote the hom bifunctor $\map {\operatorname{Hom}_{\mathbf C} } {-, -} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$.
For each object $\tuple{D^\text{op}, C} \in \mathbf D^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\paren{ {G \circ \paren{L^\text{op} \times \operatorname{id}_{\mathbf C} } } } } {D^\text{op}, C}
      | r = \map G {\map {\paren{L^\text{op} \times \operatorname{id}_{\mathbf C} } } {D^\text{op}, C} }
      | c = {{Defof|Composite Functor|Composition of Functors}}
}}
{{eqn | r = \map G {\map {L^\text{op} } {D^\text{op} }, \map {\operatorname{id}_{\mathbf C} } C}
      | c = {{Defof|Product of Functors}}
}}
{{eqn | r = \map G { \paren{L D}^\text{op}, \map {\operatorname{id}_{\mathbf C} } C}
      | c = Definition of $L^\text{op}$
}}
{{eqn | r = \map G { \paren{L D}^\text{op}, C}
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {LD, C}
      | c = {{Defof|Hom Bifunctor}}
}}
{{eqn | r = \map F {D^\text{op}, C}
      | c = {{Defof|Hom Bifunctor With Left Functor}}
}}
{{end-eqn}}
For each morphism $\tuple{f^\text{op} : D_1 \to D_2, g: C_1 \to C_2} \in \mathbf D^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\paren{ {G \circ \paren{L^\text{op} \times \operatorname{id}_{\mathbf C} } } } } {f^\text{op}, g}
      | r = \map G {\map {\paren{L^\text{op} \times \operatorname{id}_{\mathbf C} } } {f^\text{op}, g} }
      | c = {{Defof|Composite Functor|Composition of Functors}}
}}
{{eqn | r = \map G {\map {L^\text{op} } {f^\text{op} }, \map {\operatorname{id}_{\mathbf C} } g}
      | c = {{Defof|Product of Functors}}
}}
{{eqn | r = \map G { \paren{L f}^\text{op}, \map {\operatorname{id}_{\mathbf C} } g}
      | c = Definition of $L^\text{op}$
}}
{{eqn | r = \map G { \paren{L f}^\text{op}, g}
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {L f, g} : \map {\operatorname{Hom}_{\mathbf C} } {L D_1, C_1} \to \map {\operatorname{Hom}_{\mathbf C} } {L D_2, C_2} : h \mapsto g \circ h \circ L f
      | c = {{Defof|Hom Bifunctor}}
}}
{{eqn | r = \map F {f^\text{op}, g}
      | c = {{Defof|Hom Bifunctor With Left Functor}}
}}
{{end-eqn}}
The result follows.
{{qed}}