∀ (R : Type u_1) [inst : CommRing R] (C : Type u_3) [inst_1 : CategoryTheory.Category.{u_2, u_3} C]
  {W X Y Z : CategoryTheory.Free R C} (f : (W ⟶ X) →₀ R) (g : (X ⟶ Y) →₀ R) (h : (Y ⟶ Z) →₀ R),
  ((f.sum fun f' s => g.sum fun g' t => fun₀ | CategoryTheory.CategoryStruct.comp f' g' => s * t).sum fun f' s =>
      h.sum fun g' t => fun₀ | CategoryTheory.CategoryStruct.comp f' g' => s * t) =
    f.sum fun f' s =>
      (g.sum fun f' s => h.sum fun g' t => fun₀ | CategoryTheory.CategoryStruct.comp f' g' => s * t).sum fun g' t =>
        fun₀ | CategoryTheory.CategoryStruct.comp f' g' => s * t