theorem :: DUALSP06:7

for V being RealNormSpace
for x being Point of V
for y, z being Point of (DualSp V)
for a, b being Real holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))