∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f g : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (h : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (M₁.map h)
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y)) =
    CategoryTheory.CategoryStruct.comp (f.app X + g.app X) (M₂.map h)