let X be ComplexUnitarySpace; :: 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

0 <= Re (x .|. x) by Def11;
then A1: 0 <= |.(x .|. x).| by Th29;
assume ||.x.|| = 0 ; :: thesis: x = H₁(X)
then |.(x .|. x).| = 0 by A1, SQUARE_1:24;
then x .|. x = 0c by COMPLEX1:45;
hence x = H₁(X) by Def11; :: thesis: verum

end;

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