∀ {R : CommRingCat} {X Y : (AlgebraicGeometry.Spec R).Modules} (f : X ⟶ Y)
  {X_1 Y_1 : (TopologicalSpace.Opens ↥(AlgebraicGeometry.Spec R))ᵒᵖ} (i : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp (X.val.map i)
      ((ModuleCat.restrictScalars (RingCat.Hom.hom ((AlgebraicGeometry.Spec R).ringCatSheaf.val.map i))).map
        (ModuleCat.ofHom
          { toAddHom := (ModuleCat.Hom.hom ((AlgebraicGeometry.modulesSpecToSheaf.map f).val.app Y_1)).toAddHom,
            map_smul' := ⋯ })) =
    CategoryTheory.CategoryStruct.comp
      (ModuleCat.ofHom
        { toAddHom := (ModuleCat.Hom.hom ((AlgebraicGeometry.modulesSpecToSheaf.map f).val.app X_1)).toAddHom,
          map_smul' := ⋯ })
      (Y.val.map i)