theorem :: DUALSP06:8

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