theorem Th13: :: DUALSP06:13

for V being RealNormSpace
for y, z being Point of V
for x being Point of (DualSp V) holds (y - z) .|. x = (y .|. x) - (z .|. x)