∀ {C : Type u_2} {ι : Type u_3} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (i : ι),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.HomologySequence.composableArrows₂ S₁ i).map' 0 1
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_2
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_4)
      (CategoryTheory.ComposableArrows.app' (HomologicalComplex.HomologySequence.mapComposableArrows₂ φ i) 1
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_4) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ComposableArrows.app' (HomologicalComplex.HomologySequence.mapComposableArrows₂ φ i) 0
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_8)
      ((HomologicalComplex.HomologySequence.composableArrows₂ S₂ i).map' 0 1
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_2
        HomologicalComplex.HomologySequence.mapComposableArrows₅._proof_4)