Description: A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015)