∀ {M : Type u_2} {α : Type u_1} {β : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : VAdd M β]
  (f : β → α),
  (∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) → ∀ (c₁ c₂ : M) (x : β), f ((c₁ + c₂) +ᵥ x) = f (c₁ +ᵥ c₂ +ᵥ x)