∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J SemiRingCat)
  {a b :
    (j : J) →
      ↑((F.comp
              ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).comp
                (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).obj
          j)},
  a ∈
      (AddMonCat.sectionsAddSubmonoid
          (F.comp
            ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).comp
              (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))).carrier →
    b ∈
        (AddMonCat.sectionsAddSubmonoid
            (F.comp
              ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).comp
                (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))).carrier →
      a + b ∈
        (AddMonCat.sectionsAddSubmonoid
            (F.comp
              ((CategoryTheory.forget₂ SemiRingCat AddCommMonCat).comp
                (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))).carrier