let X be ComplexNormSpace; :: thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; :: thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A1: for e being Real st e > 0 holds
||.x.|| < e ; :: thesis: x = 0. X

now :: thesis: not x <> 0. X

assume x <> 0. X ; :: thesis: contradiction
then 0 <> ||.x.|| by NORMSP_0:def 5;
then 0 < ||.x.|| by CLVECT_1:105;
hence contradiction by A1; :: thesis: verum

end;

hence x = 0. X ; :: thesis: verum