∀ (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  (D : Type u_3) [inst_2 : CategoryTheory.Category.{u_4, u_3} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D]
  {X Y Z : CategoryTheory.ForgetEnrichment V D} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.eHomEquiv V).symm (CategoryTheory.ForgetEnrichment.homTo V (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V).symm (CategoryTheory.ForgetEnrichment.homTo V f))
      ((CategoryTheory.eHomEquiv V).symm (CategoryTheory.ForgetEnrichment.homTo V g))