for X being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearFunctionals X) = the carrier of X --> 0