∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N K : CategoryTheory.Mat_ C} (f : M ⟶ N) (g : N ⟶ K),
  CategoryTheory.CategoryStruct.comp f g = fun i k => ∑ j, CategoryTheory.CategoryStruct.comp (f i j) (g j k)