Description: A subcomplex pre-Hilbert space is a normed vector space. (Contributed by Mario Carneiro, 8-Oct-2015)