∀ {k : Type u_3} {V₁ : Type u_2} {V₂ : Type u_1} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module k V₂] (f : V₁ →ₗ[k] V₂) (p v : V₁), f (v + p) = f v + f p