theorem Th34: :: DUALSP01:28

for X, Y being RealNormSpace
for f being Point of (DualSp X) st f = 0. (DualSp X) holds
0 = ||.f.||