∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq)
      (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk g).hom).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv
      (CategoryTheory.Limits.imageSubobjectMap sq)