∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq] {h : CategoryTheory.Arrow C}
  [inst_4 : CategoryTheory.Limits.HasImage h.hom] (sq' : g ⟶ h) [inst_5 : CategoryTheory.Limits.HasImageMap sq'],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq'))
      (CategoryTheory.Limits.image.ι h.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom)
      (CategoryTheory.CategoryStruct.comp sq sq').right