theorem :: DUALSP06:3

for V being RealNormSpace
for x being Point of V
for y, z being Point of (DualSp V) holds x .|. (y + z) = (x .|. y) + (x .|. z) by DUALSP01:29;