theorem :: SEQ_4:62

for n being Nat
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by Th51, Th52, BINOP_2:1, FINSEQOP:74;