theorem Th26: :: DUALSP01:21

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