∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CompHaus)
  (S : CategoryTheory.Limits.Cone F) (m : S.pt ⟶ (CompHaus.limitCone F).pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp m ((CompHaus.limitCone F).π.app j) = S.π.app j) →
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp m.hom ((TopCat.limitCone (F.comp compHausToTop)).π.app j) =
        (compHausToTop.mapCone S).π.app j