∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) h