Public statement.

theorem AVenhance.Ingredients.kappaSeq_pred {β : ℝ} (I : Ingredients β) (κ : ℝ) {M m : ℕ} (hm : 1 ≤ m) (hmM : m ≤ M) : I.kappaSeq κ M (m - 1) = I.KhomScalar (I.kappaSeq κ M m) m

KBar_m^{κ_m} = κ_{m-1} (source 3897-3898: "Recall Khom_m^{κ_m} = κ_{m-1} by e.kappa.sequence").