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

assume A1: ||.x.|| = 0 ; :: thesis: x = H₁(X)
0 <= Re (x .|. x) by Def13;
then 0 <= |.(x .|. x).| by Th36;
then |.(x .|. x).| = 0 by A1, SQUARE_1:92;
then x .|. x = 0c by COMPLEX1:131;
hence x = H₁(X) by Def13; :: thesis: verum

end;

assume x = H₁(X) ; :: thesis: ||.x.|| = 0
hence ||.x.|| = 0 by Def13, COMPLEX1:130, SQUARE_1:82; :: thesis: verum