∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') {Z : CategoryTheory.Sheaf J (Type w)} (h : F' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.toImage f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.imageι f) h) =
    CategoryTheory.CategoryStruct.comp f h