∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂),
  CategoryTheory.CategoryStruct.comp φ.τ₂
      (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂).g' =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁).g' φ.τ₃