∀ {X Y Z : Type u_1} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  AddMonCat.ofHom (FreeAddMonoid.map (CategoryTheory.CategoryStruct.comp x x_1)) =
    CategoryTheory.CategoryStruct.comp (AddMonCat.ofHom (FreeAddMonoid.map x)) (AddMonCat.ofHom (FreeAddMonoid.map x_1))