∀ {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] [inst_4 : DecidableEq ι] (i : ι)
  (x₁ x₂ : M i) (y : (i : ι) → M i),
  Function.update y i '' segment 𝕜 x₁ x₂ = segment 𝕜 (Function.update y i x₁) (Function.update y i x₂)