We revisit the Vectorial λ-Calculus, a system that provides a way to model a vector space of terms by extending the classic terms of the λ-calculus with linear combination of them; and by introducing a type system on top. The system can be summarized by the slogan «If Γ ⊢ t : T and Γ ⊢ r : R then Γ ⊢ α · t + β · r : α · T + β · R».

However, the type system in Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial λ-Calculus supports the standard version of said property as well as many others in the original system, such as Progress. We also introduce the concept of weight of types and terms, and a new property relating the weight of a term with the weight of its type.M