theorem Th31: :: DUALSP01:25

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