∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₁_1 : CategoryTheory.Functor J C) (e_F₁ : F₁ = F₁_1)
  (F₂ F₂_1 : CategoryTheory.Functor J C) (e_F₂ : F₂ = F₂_1)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂],
  CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ =
    CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁_1 F₂_1