let X be RealNormSpace; :: thesis: the carrier of X --> 0 = 0. (DualSp X)
the carrier of X --> 0 = 0. (R_VectorSpace_of_BoundedLinearFunctionals X) by Th26
.= 0. (DualSp X) ;
hence the carrier of X --> 0 = 0. (DualSp X) ; :: thesis: verum