theorem Th14: :: DUALSP06:14
for V being RealNormSpace
for x being Point of V holds x .|. (0. (DualSp V)) = 0