theorem Th107: :: CLVECT_1:107

for CNS being ComplexNormSpace
for x, y being Point of CNS holds
( ||.(x - y).|| = 0 iff x = y )