theorem :: SEQ_4:65

for n being Nat
for z, z1, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2 by Lm6;