∀ {C : Type u_2} {ι : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) {A : C}
  (x : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂) ⟶ A),
  CategoryTheory.CategoryStruct.comp ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)) x = 0 →
    ∀ (hn₁ : n₀ + 1 = n₁),
      CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃ n₀ n₁ hn₁) x = 0 →
        ∀ (hn₂ : n₁ + 1 = n₂),
          CategoryTheory.CategoryStruct.comp (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ ⋯ ⋯).f x = 0