∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι),
  (F.mapMat_.obj M).X i = F.obj (M.X i)