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

proof

assume A1: ||.x.|| = 0 ; :: thesis: x = H₁(X)
0 <= x .|. x by Def2;
then x .|. x = 0 by A1, SQUARE_1:24;
hence x = H₁(X) by Def2; :: thesis: verum

end;

assume x = H₁(X) ; :: thesis: ||.x.|| = 0
hence ||.x.|| = 0 by Def2, SQUARE_1:17; :: thesis: verum