theorem :: BHSP_1:15

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