theorem Th14: :: BHSP_1:14

for X being RealUnitarySpace
for x being Point of X holds (0. X) .|. x = 0