theorem Th101: :: SEQ_4:102

for n being Nat
for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )