theorem Th6: :: DUALSP06:6

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