∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {E : Type u_4}
  [inst_8 : CategoryTheory.Category.{v_3, u_4} E] [inst_9 : CategoryTheory.Preadditive E]
  [inst_10 : CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Linear R G],
  CategoryTheory.Functor.Linear R (F.comp G)