Description: Define the function for the norm of a vector of Hilbert space. See
normval for its value and normcl for its closure. Theorems
norm-i-i , norm-ii-i , and norm-iii-i show it has the expected
properties of a norm. In the literature, the norm of A is usually
written "|| A ||", but we use function notation to take advantage of
our existing theorems about functions. Definition of norm in Beran
p. 96. (Contributed by NM, 6-Jun-2008)(New usage is discouraged.)