let X be RealUnitarySpace; :: thesis: for x being Point of X holds
( x = 0. X iff for y being Point of X holds x .|. y = 0 )
let x be Point of X; :: thesis: ( x = 0. X iff for y being Point of X holds x .|. y = 0 )

now :: thesis: ( ( for y being Point of X holds x .|. y = 0 ) implies x = 0. X )

assume for y being Point of X holds x .|. y = 0 ; :: thesis: x = 0. X
then x .|. x = 0 ;
hence x = 0. X by BHSP_1:def 2; :: thesis: verum

end;

hence ( x = 0. X iff for y being Point of X holds x .|. y = 0 ) by BHSP_1:14; :: thesis: verum