Proof of the Section 3 statement Ingredients.Khom_eq_scalar.

theorem AVenhance.Proofs.Ingredients.Khom_eq_scalar {β : ℝ} (I : Ingredients β) (κ : ℝ) (hκ : 0 < κ) (m : ℕ) (hm : 1 ≤ m) : I.Khom κ m = I.KhomScalar κ m • 1 ∧ 0 < I.KhomScalar κ m